[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
⊢ A * { coeff := inverseCoeff a A } = 1
[PROOFSTEP]
ext n
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
⊢ coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
[PROOFSTEP]
induction' n with n _
[GOAL]
case h.zero
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
⊢ coeff (A * { coeff := inverseCoeff a A }) Nat.zero = coeff 1 Nat.zero
[PROOFSTEP]
simp [WittVector.mul_coeff_zero, inverseCoeff, hA]
[GOAL]
case h.succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) = coeff 1 (Nat.succ n)
[PROOFSTEP]
let H_coeff :=
  A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) +
    nthRemainder p n (truncateFun (n + 1) A) fun i : Fin (n + 1) => inverseCoeff a A i
[GOAL]
case h.succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) = coeff 1 (Nat.succ n)
[PROOFSTEP]
have H := Units.mul_inv (a ^ p ^ (n + 1))
[GOAL]
case h.succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) = coeff 1 (Nat.succ n)
[PROOFSTEP]
linear_combination (norm := skip) -H_coeff * H
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) - coeff 1 (Nat.succ n) -
      (-H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹) - -H_coeff * 1) =
    0
[PROOFSTEP]
skip
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) - coeff 1 (Nat.succ n) -
      (-H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹) - -H_coeff * 1) =
    0
[PROOFSTEP]
have ha : (a : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1)) := by norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
[PROOFSTEP]
norm_cast
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
ha : ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) - coeff 1 (Nat.succ n) -
      (-H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹) - -H_coeff * 1) =
    0
[PROOFSTEP]
have ha_inv : (↑a⁻¹ : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹ := by norm_cast; norm_num
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
ha : ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
⊢ ↑a⁻¹ ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
ha : ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
⊢ a⁻¹ ^ p ^ (n + 1) = (a ^ p ^ (n + 1))⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
ha : ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
ha_inv : ↑a⁻¹ ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) - coeff 1 (Nat.succ n) -
      (-H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹) - -H_coeff * 1) =
    0
[PROOFSTEP]
simp only [nthRemainder_spec, inverseCoeff, succNthValUnits, hA, one_coeff_eq_of_pos, Nat.succ_pos', ha_inv, ha,
  inv_pow]
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
ha : ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
ha_inv : ↑a⁻¹ ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹
⊢ coeff A (n + 1) * ↑(a ^ p ^ (n + 1))⁻¹ +
            -↑(a ^ p ^ (n + 1))⁻¹ *
                (coeff A (n + 1) * ↑(a ^ p ^ (n + 1))⁻¹ +
                  nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i) *
              ↑(a ^ p ^ (n + 1)) +
          nthRemainder p n (truncateFun (n + 1) A) (truncateFun (n + 1) { coeff := inverseCoeff a A }) -
        0 -
      (-(coeff A (n + 1) * ↑(a ^ p ^ (n + 1))⁻¹ +
              nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i) *
          (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹) -
        -(coeff A (n + 1) * ↑(a ^ p ^ (n + 1))⁻¹ +
              nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i) *
          1) =
    0
[PROOFSTEP]
ring!
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : coeff x 0 ≠ 0
⊢ IsUnit x
[PROOFSTEP]
let y : kˣ := Units.mk0 (x.coeff 0) hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : coeff x 0 ≠ 0
y : kˣ := Units.mk0 (coeff x 0) hx
⊢ IsUnit x
[PROOFSTEP]
have hy : x.coeff 0 = y := rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : coeff x 0 ≠ 0
y : kˣ := Units.mk0 (coeff x 0) hx
hy : coeff x 0 = ↑y
⊢ IsUnit x
[PROOFSTEP]
exact (mkUnit hy).isUnit
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
⊢ Irreducible ↑p
[PROOFSTEP]
have hp : ¬IsUnit (p : 𝕎 k) := by
  intro hp
  simpa only [constantCoeff_apply, coeff_p_zero, not_isUnit_zero] using
    (constantCoeff : WittVector p k →+* _).isUnit_map hp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
⊢ ¬IsUnit ↑p
[PROOFSTEP]
intro hp
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : IsUnit ↑p
⊢ False
[PROOFSTEP]
simpa only [constantCoeff_apply, coeff_p_zero, not_isUnit_zero] using
  (constantCoeff : WittVector p k →+* _).isUnit_map hp
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
⊢ Irreducible ↑p
[PROOFSTEP]
refine' ⟨hp, fun a b hab => _⟩
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
obtain ⟨ha0, hb0⟩ : a ≠ 0 ∧ b ≠ 0 := by rw [← mul_ne_zero_iff]; intro h; rw [h] at hab ; exact p_nonzero p k hab
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
⊢ a ≠ 0 ∧ b ≠ 0
[PROOFSTEP]
rw [← mul_ne_zero_iff]
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
⊢ a * b ≠ 0
[PROOFSTEP]
intro h
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
h : a * b = 0
⊢ False
[PROOFSTEP]
rw [h] at hab
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = 0
h : a * b = 0
⊢ False
[PROOFSTEP]
exact p_nonzero p k hab
[GOAL]
case intro
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
obtain ⟨m, a, ha, rfl⟩ := verschiebung_nonzero ha0
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
b : 𝕎 k
hb0 : b ≠ 0
m : ℕ
a : 𝕎 k
ha : coeff a 0 ≠ 0
hab : ↑p = (↑verschiebung)^[m] a * b
ha0 : (↑verschiebung)^[m] a ≠ 0
⊢ IsUnit ((↑verschiebung)^[m] a) ∨ IsUnit b
[PROOFSTEP]
obtain ⟨n, b, hb, rfl⟩ := verschiebung_nonzero hb0
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
m : ℕ
a : 𝕎 k
ha : coeff a 0 ≠ 0
ha0 : (↑verschiebung)^[m] a ≠ 0
n : ℕ
b : 𝕎 k
hb : coeff b 0 ≠ 0
hb0 : (↑verschiebung)^[n] b ≠ 0
hab : ↑p = (↑verschiebung)^[m] a * (↑verschiebung)^[n] b
⊢ IsUnit ((↑verschiebung)^[m] a) ∨ IsUnit ((↑verschiebung)^[n] b)
[PROOFSTEP]
cases m
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.zero
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : coeff b 0 ≠ 0
hb0 : (↑verschiebung)^[n] b ≠ 0
ha0 : (↑verschiebung)^[Nat.zero] a ≠ 0
hab : ↑p = (↑verschiebung)^[Nat.zero] a * (↑verschiebung)^[n] b
⊢ IsUnit ((↑verschiebung)^[Nat.zero] a) ∨ IsUnit ((↑verschiebung)^[n] b)
[PROOFSTEP]
exact Or.inl (isUnit_of_coeff_zero_ne_zero a ha)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : coeff b 0 ≠ 0
hb0 : (↑verschiebung)^[n] b ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
hab : ↑p = (↑verschiebung)^[Nat.succ n✝] a * (↑verschiebung)^[n] b
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[n] b)
[PROOFSTEP]
cases' n with n
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ.zero
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
b : 𝕎 k
hb : coeff b 0 ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
hb0 : (↑verschiebung)^[Nat.zero] b ≠ 0
hab : ↑p = (↑verschiebung)^[Nat.succ n✝] a * (↑verschiebung)^[Nat.zero] b
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[Nat.zero] b)
[PROOFSTEP]
exact Or.inr (isUnit_of_coeff_zero_ne_zero b hb)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
b : 𝕎 k
hb : coeff b 0 ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
n : ℕ
hb0 : (↑verschiebung)^[Nat.succ n] b ≠ 0
hab : ↑p = (↑verschiebung)^[Nat.succ n✝] a * (↑verschiebung)^[Nat.succ n] b
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[Nat.succ n] b)
[PROOFSTEP]
rw [iterate_verschiebung_mul] at hab
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
b : 𝕎 k
hb : coeff b 0 ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
n : ℕ
hb0 : (↑verschiebung)^[Nat.succ n] b ≠ 0
hab : ↑p = (↑verschiebung)^[Nat.succ n✝ + Nat.succ n] ((↑frobenius)^[Nat.succ n] a * (↑frobenius)^[Nat.succ n✝] b)
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[Nat.succ n] b)
[PROOFSTEP]
apply_fun fun x => coeff x 1 at hab
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
b : 𝕎 k
hb : coeff b 0 ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
n : ℕ
hb0 : (↑verschiebung)^[Nat.succ n] b ≠ 0
hab :
  coeff (↑p) 1 =
    coeff ((↑verschiebung)^[Nat.succ n✝ + Nat.succ n] ((↑frobenius)^[Nat.succ n] a * (↑frobenius)^[Nat.succ n✝] b)) 1
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[Nat.succ n] b)
[PROOFSTEP]
simp only [coeff_p_one, Nat.add_succ, add_comm _ n, Function.iterate_succ', Function.comp_apply,
  verschiebung_coeff_add_one, verschiebung_coeff_zero] at hab
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
b : 𝕎 k
hb : coeff b 0 ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
n : ℕ
hb0 : (↑verschiebung)^[Nat.succ n] b ≠ 0
hab : 1 = 0
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[Nat.succ n] b)
[PROOFSTEP]
exact (one_ne_zero hab).elim
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
obtain ⟨m, c, hc, hcm⟩ := WittVector.verschiebung_nonzero ha
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
c : 𝕎 k
hc : coeff c 0 ≠ 0
hcm : a = (↑verschiebung)^[m] c
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
obtain ⟨b, rfl⟩ := (frobenius_bijective p k).surjective.iterate m c
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff ((↑frobenius)^[m] b) 0 ≠ 0
hcm : a = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
rw [WittVector.iterate_frobenius_coeff] at hc
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
have := congr_fun (WittVector.verschiebung_frobenius_comm.comp_iterate m) b
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
this : (↑verschiebung ∘ ↑frobenius)^[m] b = ((↑verschiebung)^[m] ∘ (↑frobenius)^[m]) b
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
simp only [Function.comp_apply] at this
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
rw [← this] at hcm
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
refine' ⟨m, b, _, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ coeff b 0 ≠ 0
[PROOFSTEP]
contrapose! hc
[GOAL]
case intro.intro.intro.intro.refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
hc : coeff b 0 = 0
⊢ coeff b 0 ^ p ^ m = 0
[PROOFSTEP]
have : 0 < p ^ m := pow_pos (Nat.Prime.pos Fact.out) _
[GOAL]
case intro.intro.intro.intro.refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this✝ : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
hc : coeff b 0 = 0
this : 0 < p ^ m
⊢ coeff b 0 ^ p ^ m = 0
[PROOFSTEP]
simp [hc, zero_pow this]
[GOAL]
case intro.intro.intro.intro.refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ a = ↑p ^ m * b
[PROOFSTEP]
simp_rw [← mul_left_iterate (p : 𝕎 k) m]
[GOAL]
case intro.intro.intro.intro.refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ a = (fun x => ↑p * x)^[m] b
[PROOFSTEP]
convert hcm using 2
[GOAL]
case h.e'_3.h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ (fun x => ↑p * x) = ↑verschiebung ∘ ↑frobenius
[PROOFSTEP]
ext1 x
[GOAL]
case h.e'_3.h.e'_2.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
x : 𝕎 k
⊢ ↑p * x = (↑verschiebung ∘ ↑frobenius) x
[PROOFSTEP]
rw [mul_comm, ← WittVector.verschiebung_frobenius x]
[GOAL]
case h.e'_3.h.e'_2.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
x : 𝕎 k
⊢ ↑verschiebung (↑frobenius x) = (↑verschiebung ∘ ↑frobenius) x
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
⊢ ∃ m b, a = ↑p ^ m * ↑b
[PROOFSTEP]
obtain ⟨m, b, h₁, h₂⟩ := exists_eq_pow_p_mul a ha
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : coeff b 0 ≠ 0
h₂ : a = ↑p ^ m * b
⊢ ∃ m b, a = ↑p ^ m * ↑b
[PROOFSTEP]
let b₀ := Units.mk0 (b.coeff 0) h₁
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : coeff b 0 ≠ 0
h₂ : a = ↑p ^ m * b
b₀ : kˣ := Units.mk0 (coeff b 0) h₁
⊢ ∃ m b, a = ↑p ^ m * ↑b
[PROOFSTEP]
have hb₀ : b.coeff 0 = b₀ := rfl
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : coeff b 0 ≠ 0
h₂ : a = ↑p ^ m * b
b₀ : kˣ := Units.mk0 (coeff b 0) h₁
hb₀ : coeff b 0 = ↑b₀
⊢ ∃ m b, a = ↑p ^ m * ↑b
[PROOFSTEP]
exact ⟨m, mkUnit hb₀, h₂⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
⊢ DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization (𝕎 k)
[PROOFSTEP]
refine' ⟨p, irreducible p, fun {x} hx => _⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
⊢ ∃ n, Associated (↑p ^ n) x
[PROOFSTEP]
obtain ⟨n, b, hb⟩ := exists_eq_pow_p_mul' x hx
[GOAL]
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
n : ℕ
b : (𝕎 k)ˣ
hb : x = ↑p ^ n * ↑b
⊢ ∃ n, Associated (↑p ^ n) x
[PROOFSTEP]
exact ⟨n, b, hb.symm⟩


[GOAL]
p : ℕ
R : Type u_1
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = coeff y n
⊢ x = y
[PROOFSTEP]
cases x
[GOAL]
case mk'
p : ℕ
R : Type u_1
y : 𝕎 R
coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff { coeff := coeff✝ } n = coeff y n
⊢ { coeff := coeff✝ } = y
[PROOFSTEP]
cases y
[GOAL]
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff { coeff := coeff✝¹ } n = coeff { coeff := coeff✝ } n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }
[PROOFSTEP]
simp only at h
[GOAL]
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff✝¹ n = coeff✝ n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }
[PROOFSTEP]
simp [Function.funext_iff, h]
[GOAL]
p : ℕ
R : Type u_1
x y : 𝕎 R
h : x = y
n : ℕ
⊢ coeff x n = coeff y n
[PROOFSTEP]
rw [h]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ wittZero p n = 0
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittZero p n) = ↑(map (Int.castRingHom ℚ)) 0
[PROOFSTEP]
simp only [wittZero, wittStructureRat, bind₁, aeval_zero', constantCoeff_xInTermsOfW, RingHom.map_zero, AlgHom.map_zero,
  map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ wittOne p 0 = 1
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittOne p 0) = ↑(map (Int.castRingHom ℚ)) 1
[PROOFSTEP]
simp only [wittOne, wittStructureRat, xInTermsOfW_zero, AlgHom.map_one, RingHom.map_one, bind₁_X_right,
  map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ wittOne p n = 0
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(map (Int.castRingHom ℚ)) (wittOne p n) = ↑(map (Int.castRingHom ℚ)) 0
[PROOFSTEP]
simp only [wittOne, wittStructureRat, RingHom.map_zero, AlgHom.map_one, RingHom.map_one, map_wittStructureInt]
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
[PROOFSTEP]
induction n using Nat.strong_induction_on with
| h n IH => ?_
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
[PROOFSTEP]
induction n using Nat.strong_induction_on with
| h n IH => ?_
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
[PROOFSTEP]
rw [xInTermsOfW_eq]
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑(bind₁ fun k => 1)
      ((X n - Finset.sum (Finset.range n) fun i => ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * ↑C (⅟↑p ^ n)) =
    0
[PROOFSTEP]
simp only [AlgHom.map_mul, AlgHom.map_sub, AlgHom.map_sum, AlgHom.map_pow, bind₁_X_right, bind₁_C_right]
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (1 - Finset.sum (Finset.range n) fun x => ↑C (↑p ^ x) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      ↑C (⅟↑p ^ n) =
    0
[PROOFSTEP]
rw [sub_mul, one_mul]
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (⅟↑p ^ n) -
      (Finset.sum (Finset.range n) fun x => ↑C (↑p ^ x) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        ↑C (⅟↑p ^ n) =
    0
[PROOFSTEP]
rw [Finset.sum_eq_single 0]
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (⅟↑p ^ n) - ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) * ↑C (⅟↑p ^ n) = 0
[PROOFSTEP]
simp only [invOf_eq_inv, one_mul, inv_pow, tsub_zero, RingHom.map_one, pow_zero]
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (↑p ^ n)⁻¹ - ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ n * ↑C (↑p ^ n)⁻¹ = 0
[PROOFSTEP]
simp only [one_pow, one_mul, xInTermsOfW_zero, sub_self, bind₁_X_right]
[GOAL]
case a.h.h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ∀ (b : ℕ), b ∈ Finset.range n → b ≠ 0 → ↑C (↑p ^ b) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ b) ^ p ^ (n - b) = 0
[PROOFSTEP]
intro i hin hi0
[GOAL]
case a.h.h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i ∈ Finset.range n
hi0 : i ≠ 0
⊢ ↑C (↑p ^ i) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
[PROOFSTEP]
rw [Finset.mem_range] at hin
[GOAL]
case a.h.h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i < n
hi0 : i ≠ 0
⊢ ↑C (↑p ^ i) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
[PROOFSTEP]
rw [IH _ hin (Nat.pos_of_ne_zero hi0), zero_pow (pow_pos hp.1.pos _), mul_zero]
[GOAL]
case a.h.h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ¬0 ∈ Finset.range n → ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
[PROOFSTEP]
rw [Finset.mem_range]
[GOAL]
case a.h.h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ¬0 < n → ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
[PROOFSTEP]
intro
[GOAL]
case a.h.h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
a✝ : ¬0 < n
⊢ ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
[PROOFSTEP]
contradiction
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ wittAdd p 0 = X (0, 0) + X (1, 0)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittAdd p 0) = ↑(map (Int.castRingHom ℚ)) (X (0, 0) + X (1, 0))
[PROOFSTEP]
simp only [wittAdd, wittStructureRat, AlgHom.map_add, RingHom.map_add, rename_X, xInTermsOfW_zero, map_X,
  wittPolynomial_zero, bind₁_X_right, map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ wittSub p 0 = X (0, 0) - X (1, 0)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittSub p 0) = ↑(map (Int.castRingHom ℚ)) (X (0, 0) - X (1, 0))
[PROOFSTEP]
simp only [wittSub, wittStructureRat, AlgHom.map_sub, RingHom.map_sub, rename_X, xInTermsOfW_zero, map_X,
  wittPolynomial_zero, bind₁_X_right, map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ wittMul p 0 = X (0, 0) * X (1, 0)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittMul p 0) = ↑(map (Int.castRingHom ℚ)) (X (0, 0) * X (1, 0))
[PROOFSTEP]
simp only [wittMul, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero, RingHom.map_mul,
  bind₁_X_right, AlgHom.map_mul, map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ wittNeg p 0 = -X (0, 0)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittNeg p 0) = ↑(map (Int.castRingHom ℚ)) (-X (0, 0))
[PROOFSTEP]
simp only [wittNeg, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero, RingHom.map_neg,
  AlgHom.map_neg, bind₁_X_right, map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (wittAdd p n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (X 0 + X 1) = 0
[PROOFSTEP]
simp only [add_zero, RingHom.map_add, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (wittSub p n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (X 0 - X 1) = 0
[PROOFSTEP]
simp only [sub_zero, RingHom.map_sub, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (wittMul p n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (X 0 * X 1) = 0
[PROOFSTEP]
simp only [mul_zero, RingHom.map_mul, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (wittNeg p n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (-X 0) = 0
[PROOFSTEP]
simp only [neg_zero, RingHom.map_neg, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m n : ℕ
⊢ ↑constantCoeff (wittNSMul p m n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m n : ℕ
⊢ ↑constantCoeff (m • X 0) = 0
[PROOFSTEP]
simp only [smul_zero, map_nsmul, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
z : ℤ
n : ℕ
⊢ ↑constantCoeff (wittZSMul p z n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
z : ℤ
n : ℕ
⊢ ↑constantCoeff (z • X 0) = 0
[PROOFSTEP]
simp only [smul_zero, map_zsmul, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑(aeval (Function.uncurry fun i => ![].coeff)) (wittZero p n) = 0
[PROOFSTEP]
simp only [wittZero_eq_zero, AlgHom.map_zero]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(aeval (Function.uncurry fun i => ![].coeff)) (wittOne p 0) = 1
[PROOFSTEP]
simp only [wittOne_zero_eq_one, AlgHom.map_one]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(aeval (Function.uncurry fun i => ![].coeff)) (wittOne p n) = 0
[PROOFSTEP]
simp only [hn, wittOne_pos_eq_zero, AlgHom.map_zero]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
i : Fin 2
⊢ (Matrix.vecCons x ![y] i).coeff = Matrix.vecCons x.coeff ![y.coeff] i
[PROOFSTEP]
fin_cases i
[GOAL]
case head
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
⊢ (Matrix.vecCons x ![y] { val := 0, isLt := (_ : 0 < 2) }).coeff =
    Matrix.vecCons x.coeff ![y.coeff] { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp
[GOAL]
case tail.head
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
⊢ (Matrix.vecCons x ![y] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).coeff =
    Matrix.vecCons x.coeff ![y.coeff] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ coeff (x + y) n = peval (wittAdd p n) ![x.coeff, y.coeff]
[PROOFSTEP]
simp [(· + ·), Add.add, eval, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ coeff (x - y) n = peval (wittSub p n) ![x.coeff, y.coeff]
[PROOFSTEP]
simp [(· - ·), Sub.sub, eval, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ coeff (x * y) n = peval (wittMul p n) ![x.coeff, y.coeff]
[PROOFSTEP]
simp [(· * ·), Mul.mul, eval, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ coeff (-x) n = peval (wittNeg p n) ![x.coeff]
[PROOFSTEP]
simp [Neg.neg, eval, Matrix.cons_fin_one, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ coeff (m • x) n = peval (wittNSMul p m n) ![x.coeff]
[PROOFSTEP]
simp [(· • ·), SMul.smul, eval, Matrix.cons_fin_one, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m : ℤ
x : 𝕎 R
n : ℕ
⊢ coeff (m • x) n = peval (wittZSMul p m n) ![x.coeff]
[PROOFSTEP]
simp [(· • ·), SMul.smul, eval, Matrix.cons_fin_one, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ coeff (x ^ m) n = peval (wittPow p m n) ![x.coeff]
[PROOFSTEP]
simp [(· ^ ·), Pow.pow, eval, Matrix.cons_fin_one, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ coeff (x + y) 0 = coeff x 0 + coeff y 0
[PROOFSTEP]
simp [add_coeff, peval]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ coeff (x * y) 0 = coeff x 0 * coeff y 0
[PROOFSTEP]
simp [mul_coeff, peval]


[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ↑(ghostComponent n) (teichmullerFun p r) = r ^ p ^ n
[PROOFSTEP]
rw [ghostComponent_apply, aeval_wittPolynomial, Finset.sum_eq_single 0, pow_zero, one_mul, tsub_zero]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ coeff (teichmullerFun p r) 0 ^ p ^ n = r ^ p ^ n
[PROOFSTEP]
rfl
[GOAL]
case h₀
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ∀ (b : ℕ), b ∈ Finset.range (n + 1) → b ≠ 0 → ↑p ^ b * coeff (teichmullerFun p r) b ^ p ^ (n - b) = 0
[PROOFSTEP]
intro i hi h0
[GOAL]
case h₀
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ ↑p ^ i * coeff (teichmullerFun p r) i ^ p ^ (n - i) = 0
[PROOFSTEP]
convert mul_zero (M₀ := R) _
[GOAL]
case h.e'_2.h.e'_6
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ coeff (teichmullerFun p r) i ^ p ^ (n - i) = 0
[PROOFSTEP]
convert zero_pow (M := R) _
[GOAL]
case h.e'_2.h.e'_5
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ coeff (teichmullerFun p r) i = 0
[PROOFSTEP]
cases i
[GOAL]
case h.e'_2.h.e'_5.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
hi : Nat.zero ∈ Finset.range (n + 1)
h0 : Nat.zero ≠ 0
⊢ coeff (teichmullerFun p r) Nat.zero = 0
[PROOFSTEP]
contradiction
[GOAL]
case h.e'_2.h.e'_5.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n n✝ : ℕ
hi : Nat.succ n✝ ∈ Finset.range (n + 1)
h0 : Nat.succ n✝ ≠ 0
⊢ coeff (teichmullerFun p r) (Nat.succ n✝) = 0
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2.h.e'_6.convert_2
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ 0 < p ^ (n - i)
[PROOFSTEP]
exact pow_pos hp.1.pos _
[GOAL]
case h₁
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ¬0 ∈ Finset.range (n + 1) → ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
[PROOFSTEP]
rw [Finset.mem_range]
[GOAL]
case h₁
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ¬0 < n + 1 → ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
[PROOFSTEP]
intro h
[GOAL]
case h₁
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
h : ¬0 < n + 1
⊢ ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
[PROOFSTEP]
exact (h (Nat.succ_pos n)).elim
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ ↑(map f) (teichmullerFun p r) = teichmullerFun p (↑f r)
[PROOFSTEP]
ext n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n : ℕ
⊢ coeff (↑(map f) (teichmullerFun p r)) n = coeff (teichmullerFun p (↑f r)) n
[PROOFSTEP]
cases n
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ coeff (↑(map f) (teichmullerFun p r)) Nat.zero = coeff (teichmullerFun p (↑f r)) Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n✝ : ℕ
⊢ coeff (↑(map f) (teichmullerFun p r)) (Nat.succ n✝) = coeff (teichmullerFun p (↑f r)) (Nat.succ n✝)
[PROOFSTEP]
exact f.map_zero
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y
[PROOFSTEP]
apply (ghostMap.bijective_of_invertible p (MvPolynomial R ℚ)).1
[GOAL]
case a
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
⊢ ↑ghostMap (teichmullerFun p (x * y)) = ↑ghostMap (teichmullerFun p x * teichmullerFun p y)
[PROOFSTEP]
rw [RingHom.map_mul]
[GOAL]
case a
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
⊢ ↑ghostMap (teichmullerFun p (x * y)) = ↑ghostMap (teichmullerFun p x) * ↑ghostMap (teichmullerFun p y)
[PROOFSTEP]
ext1 n
[GOAL]
case a.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
n : ℕ
⊢ ↑ghostMap (teichmullerFun p (x * y)) n = (↑ghostMap (teichmullerFun p x) * ↑ghostMap (teichmullerFun p y)) n
[PROOFSTEP]
simp only [Pi.mul_apply, ghostMap_apply, ghostComponent_teichmullerFun, mul_pow]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℤ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y
[PROOFSTEP]
refine' map_injective (MvPolynomial.map (Int.castRingHom ℚ)) (MvPolynomial.map_injective _ Int.cast_injective) _
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℤ
⊢ ↑(map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p (x * y)) =
    ↑(map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p x * teichmullerFun p y)
[PROOFSTEP]
simp only [teichmuller_mul_aux₁, map_teichmullerFun, RingHom.map_mul]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ teichmullerFun p 1 = 1
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ coeff (teichmullerFun p 1) Nat.zero = coeff 1 Nat.zero
[PROOFSTEP]
rw [one_coeff_zero]
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ coeff (teichmullerFun p 1) Nat.zero = 1
[PROOFSTEP]
rfl
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (teichmullerFun p 1) (Nat.succ n✝) = coeff 1 (Nat.succ n✝)
[PROOFSTEP]
rw [one_coeff_eq_of_pos _ _ _ (Nat.succ_pos _)]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (teichmullerFun p 1) (Nat.succ n✝) = 0
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (x y : R),
    OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (x * y) =
      OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } x *
        OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } y
[PROOFSTEP]
intro x y
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : R
⊢ OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (x * y) =
    OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } x *
      OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } y
[PROOFSTEP]
rcases counit_surjective R x with ⟨x, rfl⟩
[GOAL]
case intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
y : R
x : MvPolynomial R ℤ
⊢ OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (↑(counit R) x * y) =
    OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (↑(counit R) x) *
      OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } y
[PROOFSTEP]
rcases counit_surjective R y with ⟨y, rfl⟩
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℤ
⊢ OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (↑(counit R) x * ↑(counit R) y) =
    OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (↑(counit R) x) *
      OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (↑(counit R) y)
[PROOFSTEP]
simp only [← map_teichmullerFun, ← RingHom.map_mul, teichmuller_mul_aux₂]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ↑(teichmuller p) 0 = 0
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ coeff (↑(teichmuller p) 0) Nat.zero = coeff 0 Nat.zero
[PROOFSTEP]
rw [zero_coeff]
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ coeff (↑(teichmuller p) 0) Nat.zero = 0
[PROOFSTEP]
rfl
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (↑(teichmuller p) 0) (Nat.succ n✝) = coeff 0 (Nat.succ n✝)
[PROOFSTEP]
rw [zero_coeff]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (↑(teichmuller p) 0) (Nat.succ n✝) = 0
[PROOFSTEP]
rfl


[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(bind₁ (frobeniusPolyRat p)) (wittPolynomial p ℚ n) = wittPolynomial p ℚ (n + 1)
[PROOFSTEP]
delta frobeniusPolyRat
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(bind₁ fun n => ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)) (wittPolynomial p ℚ n) =
    wittPolynomial p ℚ (n + 1)
[PROOFSTEP]
rw [← bind₁_bind₁, bind₁_xInTermsOfW_wittPolynomial, bind₁_X_right, Function.comp_apply]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ frobeniusPolyAux p n =
    X (n + 1) -
      ∑ i in range n,
        ∑ j in range (p ^ (n - i)),
          (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (j + 1) /
                    p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                  p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))
[PROOFSTEP]
rw [frobeniusPolyAux, ← Fin.sum_univ_eq_sum_range]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n j : ℕ
hj : j < p ^ n
⊢ p ^ (n - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) ∣ Nat.choose (p ^ n) (j + 1)
[PROOFSTEP]
apply multiplicity.pow_dvd_of_le_multiplicity
[GOAL]
case a
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n j : ℕ
hj : j < p ^ n
⊢ ↑(n - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) ≤ multiplicity p (Nat.choose (p ^ n) (j + 1))
[PROOFSTEP]
rw [hp.out.multiplicity_choose_prime_pow hj j.succ_ne_zero]
[GOAL]
case a
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n j : ℕ
hj : j < p ^ n
⊢ ↑(n - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) ≤
    ↑(n - Part.get (multiplicity p (Nat.succ j)) (_ : multiplicity.Finite p (Nat.succ j)))
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
⊢ j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) } + n =
    i + j + (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
[PROOFSTEP]
generalize h : v p ⟨j + 1, j.succ_pos⟩ = m
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p { val := j + 1, property := (_ : 0 < Nat.succ j) } = m
⊢ j - m + n = i + j + (n - i - m)
[PROOFSTEP]
rsuffices ⟨h₁, h₂⟩ : m ≤ n - i ∧ m ≤ j
[GOAL]
case intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p { val := j + 1, property := (_ : 0 < Nat.succ j) } = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j - m + n = i + j + (n - i - m)
[PROOFSTEP]
rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)), add_assoc, tsub_right_comm,
  add_comm i, tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p { val := j + 1, property := (_ : 0 < Nat.succ j) } = m
⊢ m ≤ n - i ∧ m ≤ j
[PROOFSTEP]
have hle : p ^ m ≤ j + 1 := h ▸ Nat.le_of_dvd j.succ_pos (multiplicity.pow_multiplicity_dvd _)
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p { val := j + 1, property := (_ : 0 < Nat.succ j) } = m
hle : p ^ m ≤ j + 1
⊢ m ≤ n - i ∧ m ≤ j
[PROOFSTEP]
exact ⟨(pow_le_pow_iff hp.1.one_lt).1 (hle.trans hj), Nat.le_of_lt_succ ((Nat.lt_pow_self hp.1.one_lt m).trans_le hle)⟩
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPoly p n) = frobeniusPolyRat p n
[PROOFSTEP]
rw [frobeniusPoly, RingHom.map_add, RingHom.map_mul, RingHom.map_pow, map_C, map_X, eq_intCast, Int.cast_ofNat,
  frobeniusPolyRat]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
[PROOFSTEP]
refine Nat.strong_induction_on n ?_
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ),
        m < n →
          X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
            ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)) →
      X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
[PROOFSTEP]
clear n
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ),
        m < n →
          X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
            ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)) →
      X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
[PROOFSTEP]
intro n IH
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
⊢ X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
[PROOFSTEP]
rw [xInTermsOfW_eq]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
⊢ X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1))
      ((X n - ∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * ↑C (⅟↑p ^ n))
[PROOFSTEP]
simp only [AlgHom.map_sum, AlgHom.map_sub, AlgHom.map_mul, AlgHom.map_pow, bind₁_C_right]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
⊢ X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (X n) -
        ∑ x in range n,
          ↑C (↑p ^ x) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      ↑C (⅟↑p ^ n)
[PROOFSTEP]
have h1 : (p : ℚ) ^ n * ⅟(p : ℚ) ^ n = 1 := by rw [← mul_pow, mul_invOf_self, one_pow]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
⊢ ↑p ^ n * ⅟↑p ^ n = 1
[PROOFSTEP]
rw [← mul_pow, mul_invOf_self, one_pow]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (X n) -
        ∑ x in range n,
          ↑C (↑p ^ x) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      ↑C (⅟↑p ^ n)
[PROOFSTEP]
rw [bind₁_X_right, Function.comp_apply, wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ, sum_range_succ, tsub_self,
  add_tsub_cancel_left, pow_zero, pow_one, pow_one, sub_mul, add_mul, add_mul, mul_right_comm,
  mul_right_comm (C ((p : ℚ) ^ (n + 1))), ← C_mul, ← C_mul, pow_succ, mul_assoc (p : ℚ) ((p : ℚ) ^ n), h1, mul_one, C_1,
  one_mul, add_comm _ (X n ^ p), add_assoc, ← add_sub, add_right_inj, frobeniusPolyAux_eq, RingHom.map_sub, map_X,
  mul_sub, sub_eq_add_neg, add_comm _ (C (p : ℚ) * X (n + 1)), ← add_sub,
  show (Int.castRingHom ℚ) ↑p = (p : ℚ) from rfl, add_right_inj, neg_eq_iff_eq_neg, neg_sub, eq_comm]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ (∑ x in range n, ↑C (↑p ^ x) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        ↑C (⅟↑p ^ n) -
      (∑ x in range n, ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * ↑C (⅟↑p ^ n) =
    ↑C ↑p *
      ↑(MvPolynomial.map (Int.castRingHom ℚ))
        (∑ i in range n,
          ∑ j in range (p ^ (n - i)),
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
              ↑C
                ↑(Nat.choose (p ^ (n - i)) (j + 1) /
                      p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                    p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })))
[PROOFSTEP]
simp only [map_sum, mul_sum, sum_mul, ← sum_sub_distrib]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ ∑ x in range n,
      (↑C (↑p ^ x) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x) * ↑C (⅟↑p ^ n) -
        ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x) * ↑C (⅟↑p ^ n)) =
    ∑ x in range n,
      ∑ x_1 in range (p ^ (n - x)),
        ↑C ↑p *
          ↑(MvPolynomial.map (Int.castRingHom ℚ))
            ((X x ^ p) ^ (p ^ (n - x) - (x_1 + 1)) * frobeniusPolyAux p x ^ (x_1 + 1) *
              ↑C
                ↑(Nat.choose (p ^ (n - x)) (x_1 + 1) /
                      p ^ (n - x - v p { val := x_1 + 1, property := (_ : 0 < Nat.succ x_1) }) *
                    p ^ (x_1 - v p { val := x_1 + 1, property := (_ : 0 < Nat.succ x_1) })))
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ ∀ (x : ℕ),
    x ∈ range n →
      ↑C (↑p ^ x) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x) * ↑C (⅟↑p ^ n) -
          ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x) * ↑C (⅟↑p ^ n) =
        ∑ x_1 in range (p ^ (n - x)),
          ↑C ↑p *
            ↑(MvPolynomial.map (Int.castRingHom ℚ))
              ((X x ^ p) ^ (p ^ (n - x) - (x_1 + 1)) * frobeniusPolyAux p x ^ (x_1 + 1) *
                ↑C
                  ↑(Nat.choose (p ^ (n - x)) (x_1 + 1) /
                        p ^ (n - x - v p { val := x_1 + 1, property := (_ : 0 < Nat.succ x_1) }) *
                      p ^ (x_1 - v p { val := x_1 + 1, property := (_ : 0 < Nat.succ x_1) })))
[PROOFSTEP]
intro i hi
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i ∈ range n
⊢ ↑C (↑p ^ i) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ i) ^ p ^ (n - i) * ↑C (⅟↑p ^ n) -
      ↑C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * ↑C (⅟↑p ^ n) =
    ∑ x in range (p ^ (n - i)),
      ↑C ↑p *
        ↑(MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                    p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                  p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
rw [mem_range] at hi
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ ↑C (↑p ^ i) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ i) ^ p ^ (n - i) * ↑C (⅟↑p ^ n) -
      ↑C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * ↑C (⅟↑p ^ n) =
    ∑ x in range (p ^ (n - i)),
      ↑C ↑p *
        ↑(MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                    p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                  p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
rw [← IH i hi]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ ↑C (↑p ^ i) *
          (X i ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^
            p ^ (n - i) *
        ↑C (⅟↑p ^ n) -
      ↑C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * ↑C (⅟↑p ^ n) =
    ∑ x in range (p ^ (n - i)),
      ↑C ↑p *
        ↑(MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                    p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                  p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
clear IH
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ ↑C (↑p ^ i) *
          (X i ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^
            p ^ (n - i) *
        ↑C (⅟↑p ^ n) -
      ↑C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * ↑C (⅟↑p ^ n) =
    ∑ x in range (p ^ (n - i)),
      ↑C ↑p *
        ↑(MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                    p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                  p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
rw [add_comm (X i ^ p), add_pow, sum_range_succ', pow_zero, tsub_zero, Nat.choose_zero_right, one_mul, Nat.cast_one,
  mul_one, mul_add, add_mul, Nat.succ_sub (le_of_lt hi), Nat.succ_eq_add_one (n - i), pow_succ, pow_mul, add_sub_cancel,
  mul_sum, sum_mul]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ ∑ x in range (p ^ (n - i)),
      ↑C (↑p ^ i) *
          ((↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (x + 1) *
              (X i ^ p) ^ (p ^ (n - i) - (x + 1)) *
            ↑(Nat.choose (p ^ (n - i)) (x + 1))) *
        ↑C (⅟↑p ^ n) =
    ∑ x in range (p ^ (n - i)),
      ↑C ↑p *
        ↑(MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                    p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                  p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ ∀ (x : ℕ),
    x ∈ range (p ^ (n - i)) →
      ↑C (↑p ^ i) *
            ((↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (x + 1) *
                (X i ^ p) ^ (p ^ (n - i) - (x + 1)) *
              ↑(Nat.choose (p ^ (n - i)) (x + 1))) *
          ↑C (⅟↑p ^ n) =
        ↑C ↑p *
          ↑(MvPolynomial.map (Int.castRingHom ℚ))
            ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
              ↑C
                ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                      p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                    p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
intro j hj
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j ∈ range (p ^ (n - i))
⊢ ↑C (↑p ^ i) *
        ((↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑(Nat.choose (p ^ (n - i)) (j + 1))) *
      ↑C (⅟↑p ^ n) =
    ↑C ↑p *
      ↑(MvPolynomial.map (Int.castRingHom ℚ))
        ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
          ↑C
            ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })))
[PROOFSTEP]
rw [mem_range] at hj
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑C (↑p ^ i) *
        ((↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑(Nat.choose (p ^ (n - i)) (j + 1))) *
      ↑C (⅟↑p ^ n) =
    ↑C ↑p *
      ↑(MvPolynomial.map (Int.castRingHom ℚ))
        ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
          ↑C
            ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })))
[PROOFSTEP]
rw [RingHom.map_mul, RingHom.map_mul, RingHom.map_pow, RingHom.map_pow, RingHom.map_pow, RingHom.map_pow,
  RingHom.map_pow, map_C, map_X, mul_pow]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑C ↑p ^ i *
        (↑C (↑(Int.castRingHom ℚ) ↑p) ^ (j + 1) *
              ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑(Nat.choose (p ^ (n - i)) (j + 1))) *
      ↑C ⅟↑p ^ n =
    ↑C ↑p *
      ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        ↑C
          (↑(Int.castRingHom ℚ)
            ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))))
[PROOFSTEP]
rw [mul_comm (C (p : ℚ) ^ i), mul_comm _ ((X i ^ p) ^ _), show (Int.castRingHom ℚ) ↑p = (p : ℚ) from rfl,
  mul_comm (C (p : ℚ) ^ (j + 1)), mul_comm (C (p : ℚ))]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
            (↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * ↑C ↑p ^ (j + 1)) *
          ↑(Nat.choose (p ^ (n - i)) (j + 1)) *
        ↑C ↑p ^ i *
      ↑C ⅟↑p ^ n =
    (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        ↑C
          (↑(Int.castRingHom ℚ)
            ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) *
      ↑C ↑p
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
      (↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        (↑C ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑C ↑p ^ i * ↑C ⅟↑p ^ n)))) =
    (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
      (↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        (↑C
            (↑(Int.castRingHom ℚ)
              ↑(Nat.choose (p ^ (n - i)) (j + 1) /
                    p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                  p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) *
          ↑C ↑p))
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
      (↑C ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑C ↑p ^ i * ↑C ⅟↑p ^ n))) =
    ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
      (↑C
          (↑(Int.castRingHom ℚ)
            ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) *
        ↑C ↑p)
[PROOFSTEP]
apply congr_arg
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑C ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑C ↑p ^ i * ↑C ⅟↑p ^ n)) =
    ↑C
        (↑(Int.castRingHom ℚ)
          ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
              p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) *
      ↑C ↑p
[PROOFSTEP]
rw [← C_eq_coe_nat]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑C ↑p ^ (j + 1) * (↑C ↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑C ↑p ^ i * ↑C ⅟↑p ^ n)) =
    ↑C
        (↑(Int.castRingHom ℚ)
          ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
              p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) *
      ↑C ↑p
[PROOFSTEP]
simp only [← RingHom.map_pow, ← C_mul]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑C (↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * ⅟↑p ^ n))) =
    ↑C
      (↑(Int.castRingHom ℚ)
          ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
              p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
        ↑p)
[PROOFSTEP]
rw [C_inj]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * ⅟↑p ^ n)) =
    ↑(Int.castRingHom ℚ)
        ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
            p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
      ↑p
[PROOFSTEP]
simp only [invOf_eq_inv, eq_intCast, inv_pow, Int.cast_ofNat, Nat.cast_mul, Int.cast_mul]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
        ↑(p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
      ↑p
[PROOFSTEP]
rw [Rat.coe_nat_div _ _ (map_frobeniusPoly.key₁ p (n - i) j hj)]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑(Nat.choose (p ^ (n - i)) (j + 1)) / ↑(p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
        ↑(p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
      ↑p
[PROOFSTEP]
simp only [Nat.cast_pow, pow_add, pow_one]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ j * ↑p * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑(Nat.choose (p ^ (n - i)) (j + 1)) / ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
        ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
      ↑p
[PROOFSTEP]
suffices
  (((p ^ (n - i)).choose (j + 1) : ℚ) * (p : ℚ) ^ (j - v p ⟨j + 1, j.succ_pos⟩) * ↑p * (p ^ n : ℚ)) =
    (p : ℚ) ^ j * p * ↑((p ^ (n - i)).choose (j + 1) * p ^ i) * (p : ℚ) ^ (n - i - v p ⟨j + 1, j.succ_pos⟩)
  by
  have aux : ∀ k : ℕ, (p : ℚ) ^ k ≠ 0 := by intro; apply pow_ne_zero; exact_mod_cast hp.1.ne_zero
  simpa [aux, -one_div, field_simps] using this.symm
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
this :
  ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
⊢ ↑p ^ j * ↑p * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑(Nat.choose (p ^ (n - i)) (j + 1)) / ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
        ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
      ↑p
[PROOFSTEP]
have aux : ∀ k : ℕ, (p : ℚ) ^ k ≠ 0 := by intro; apply pow_ne_zero; exact_mod_cast hp.1.ne_zero
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
this :
  ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
⊢ ∀ (k : ℕ), ↑p ^ k ≠ 0
[PROOFSTEP]
intro
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
this :
  ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
k✝ : ℕ
⊢ ↑p ^ k✝ ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
this :
  ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
k✝ : ℕ
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.1.ne_zero
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
this :
  ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
aux : ∀ (k : ℕ), ↑p ^ k ≠ 0
⊢ ↑p ^ j * ↑p * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑(Nat.choose (p ^ (n - i)) (j + 1)) / ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
        ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
      ↑p
[PROOFSTEP]
simpa [aux, -one_div, field_simps] using this.symm
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
[PROOFSTEP]
rw [mul_comm _ (p : ℚ), mul_assoc, Nat.cast_pow, mul_assoc, ← pow_add, map_frobeniusPoly.key₂ p hi.le hj, Nat.cast_mul,
  Nat.cast_pow]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p *
      (↑(Nat.choose (p ^ (n - i)) (j + 1)) *
        ↑p ^ (i + j + (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) =
    ↑p ^ j * ↑p * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
[PROOFSTEP]
ring
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n) = X n ^ p
[PROOFSTEP]
rw [frobeniusPoly, RingHom.map_add, RingHom.map_pow, RingHom.map_mul, map_X, map_C]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ X n ^ p +
      ↑C (↑(Int.castRingHom (ZMod p)) ↑p) * ↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPolyAux p n) =
    X n ^ p
[PROOFSTEP]
simp only [Int.cast_ofNat, add_zero, eq_intCast, ZMod.nat_cast_self, zero_mul, C_0]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(bind₁ (frobeniusPoly p)) (wittPolynomial p ℤ n) = wittPolynomial p ℤ (n + 1)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (↑(bind₁ (frobeniusPoly p)) (wittPolynomial p ℤ n)) =
    ↑(MvPolynomial.map (Int.castRingHom ℚ)) (wittPolynomial p ℤ (n + 1))
[PROOFSTEP]
simp only [map_bind₁, map_frobeniusPoly, bind₁_frobeniusPolyRat_wittPolynomial, map_wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ coeff (frobeniusFun x) n = ↑(aeval x.coeff) (frobeniusPoly p n)
[PROOFSTEP]
rw [frobeniusFun, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ ⦃R : Type ?u.420485⦄ [inst : CommRing R] (x : 𝕎 R),
    (frobeniusFun x).coeff = fun n => ↑(aeval x.coeff) (frobeniusPoly p n)
[PROOFSTEP]
intros
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
R✝ : Type ?u.420485
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ (frobeniusFun x✝).coeff = fun n => ↑(aeval x✝.coeff) (frobeniusPoly p n)
[PROOFSTEP]
funext n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
R✝ : Type ?u.420485
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ coeff (frobeniusFun x✝) n = ↑(aeval x✝.coeff) (frobeniusPoly p n)
[PROOFSTEP]
apply coeff_frobeniusFun
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
x : 𝕎 R
⊢ ↑(ghostComponent n) (frobeniusFun x) = ↑(ghostComponent (n + 1)) x
[PROOFSTEP]
simp only [ghostComponent_apply, frobeniusFun, coeff_mk, ← bind₁_frobeniusPoly_wittPolynomial, aeval_bind₁]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ frobeniusFun 1 = 1
[PROOFSTEP]
refine
  -- Porting note: removing the placeholders give an errorIsPoly.ext
    (@IsPoly.comp p _ _ (frobeniusFun_isPoly p) WittVector.oneIsPoly)
    (@IsPoly.comp p _ _ WittVector.oneIsPoly (frobeniusFun_isPoly p)) ?_ _ 0
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    ↑(ghostComponent n) ((frobeniusFun ∘ fun x => 1) x) = ↑(ghostComponent n) (((fun x => 1) ∘ frobeniusFun) x)
[PROOFSTEP]
simp only [Function.comp_apply, map_one, forall_const]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (n : ℕ), ↑(ghostComponent n) (frobeniusFun 1) = 1
[PROOFSTEP]
ghost_simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (x y : 𝕎 R),
    OneHom.toFun
        { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
        (x * y) =
      OneHom.toFun
          { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
          x *
        OneHom.toFun
          { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) } y
[PROOFSTEP]
ghost_calc _ _
[GOAL]
case refine_3
p : ℕ
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : CommRing S
R : Type u_1
R._inst : CommRing R
x✝ y✝ : 𝕎 R
⊢ ∀ (n : ℕ),
    ↑(ghostComponent n)
        (OneHom.toFun
          { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
          (x✝ * y✝)) =
      ↑(ghostComponent n)
        (OneHom.toFun
            { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
            x✝ *
          OneHom.toFun
            { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
            y✝)
[PROOFSTEP]
ghost_simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := frobeniusFun,
              map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
          map_mul' :=
            (_ :
              ∀ (x y : 𝕎 R),
                OneHom.toFun
                    { toFun := frobeniusFun,
                      map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := frobeniusFun,
                        map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                      x *
                    OneHom.toFun
                      { toFun := frobeniusFun,
                        map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                      y) })
      0 =
    0
[PROOFSTEP]
refine
  IsPoly.ext (@IsPoly.comp p _ _ (frobeniusFun_isPoly p) WittVector.zeroIsPoly)
    (@IsPoly.comp p _ _ WittVector.zeroIsPoly (frobeniusFun_isPoly p)) ?_ _ 0
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    ↑(ghostComponent n) ((frobeniusFun ∘ fun x => 0) x) = ↑(ghostComponent n) (((fun x => 0) ∘ frobeniusFun) x)
[PROOFSTEP]
simp only [Function.comp_apply, map_zero, forall_const]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (n : ℕ), ↑(ghostComponent n) (frobeniusFun 0) = 0
[PROOFSTEP]
ghost_simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (x y : 𝕎 R),
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := frobeniusFun,
                map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
            map_mul' :=
              (_ :
                ∀ (x y : 𝕎 R),
                  OneHom.toFun
                      { toFun := frobeniusFun,
                        map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := frobeniusFun,
                          map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                        x *
                      OneHom.toFun
                        { toFun := frobeniusFun,
                          map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                        y) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := frobeniusFun,
                  map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
              map_mul' :=
                (_ :
                  ∀ (x y : 𝕎 R),
                    OneHom.toFun
                        { toFun := frobeniusFun,
                          map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          x *
                        OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := frobeniusFun,
                  map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
              map_mul' :=
                (_ :
                  ∀ (x y : 𝕎 R),
                    OneHom.toFun
                        { toFun := frobeniusFun,
                          map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          x *
                        OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          y) })
          y
[PROOFSTEP]
ghost_calc _ _
[GOAL]
case refine_3
p : ℕ
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : CommRing S
R : Type u_1
R._inst : CommRing R
x✝ y✝ : 𝕎 R
⊢ ∀ (n : ℕ),
    ↑(ghostComponent n)
        (OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := frobeniusFun,
                  map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
              map_mul' :=
                (_ :
                  ∀ (x y : 𝕎 R),
                    OneHom.toFun
                        { toFun := frobeniusFun,
                          map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          x *
                        OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          y) })
          (x✝ + y✝)) =
      ↑(ghostComponent n)
        (OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := frobeniusFun,
                    map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
                map_mul' :=
                  (_ :
                    ∀ (x y : 𝕎 R),
                      OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := frobeniusFun,
                              map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                            x *
                          OneHom.toFun
                            { toFun := frobeniusFun,
                              map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                            y) })
            x✝ +
          OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := frobeniusFun,
                    map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
                map_mul' :=
                  (_ :
                    ∀ (x y : 𝕎 R),
                      OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := frobeniusFun,
                              map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                            x *
                          OneHom.toFun
                            { toFun := frobeniusFun,
                              map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                            y) })
            y✝)
[PROOFSTEP]
ghost_simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ coeff (↑frobenius x) n = coeff x n ^ p
[PROOFSTEP]
rw [coeff_frobenius]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ ↑(aeval x.coeff) (frobeniusPoly p n) = coeff x n ^ p
[PROOFSTEP]
letI : Algebra (ZMod p) R :=
  ZMod.algebra _
    _
      -- outline of the calculation, proofs follow below
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ ↑(aeval x.coeff) (frobeniusPoly p n) = coeff x n ^ p
[PROOFSTEP]
calc
  aeval (fun k => x.coeff k) (frobeniusPoly p n) =
      aeval (fun k => x.coeff k) (MvPolynomial.map (Int.castRingHom (ZMod p)) (frobeniusPoly p n)) :=
    ?_
  _ = aeval (fun k => x.coeff k) (X n ^ p : MvPolynomial ℕ (ZMod p)) := ?_
  _ = x.coeff n ^ p := ?_
[GOAL]
case calc_1
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ ↑(aeval fun k => coeff x k) (frobeniusPoly p n) =
    ↑(aeval fun k => coeff x k) (↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))
[PROOFSTEP]
conv_rhs => rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(aeval fun k => coeff x k) (↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))
[PROOFSTEP]
rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(aeval fun k => coeff x k) (↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))
[PROOFSTEP]
rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(aeval fun k => coeff x k) (↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))
[PROOFSTEP]
rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
[GOAL]
case calc_1
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ ↑(aeval fun k => coeff x k) (frobeniusPoly p n) =
    ↑(eval₂Hom (RingHom.comp (algebraMap (ZMod p) R) (Int.castRingHom (ZMod p))) fun k => coeff x k) (frobeniusPoly p n)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
[GOAL]
case calc_2
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ ↑(aeval fun k => coeff x k) (↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n)) =
    ↑(aeval fun k => coeff x k) (X n ^ p)
[PROOFSTEP]
rw [frobeniusPoly_zmod]
[GOAL]
case calc_3
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ ↑(aeval fun k => coeff x k) (X n ^ p) = coeff x n ^ p
[PROOFSTEP]
rw [map_pow, aeval_X]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
⊢ frobenius = map (_root_.frobenius R p)
[PROOFSTEP]
ext (x n)
[GOAL]
case a.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ coeff (↑frobenius x) n = coeff (↑(map (_root_.frobenius R p)) x) n
[PROOFSTEP]
simp only [coeff_frobenius_charP, map_coeff, frobenius_def]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 (ZMod p)
⊢ ↑frobenius x = x
[PROOFSTEP]
simp only [ext_iff, coeff_frobenius_charP, ZMod.pow_card, eq_self_iff_true, forall_const]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
src✝ : 𝕎 R →+* 𝕎 R := frobenius
f : 𝕎 R
n : ℕ
⊢ coeff (↑(map ↑(RingEquiv.symm (_root_.frobeniusEquiv R p))) (↑frobenius f)) n = coeff f n
[PROOFSTEP]
rw [frobenius_eq_map_frobenius]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
src✝ : 𝕎 R →+* 𝕎 R := frobenius
f : 𝕎 R
n : ℕ
⊢ coeff (↑(map ↑(RingEquiv.symm (_root_.frobeniusEquiv R p))) (↑(map (_root_.frobenius R p)) f)) n = coeff f n
[PROOFSTEP]
exact frobeniusEquiv_symm_apply_frobenius R p _
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
src✝ : 𝕎 R →+* 𝕎 R := frobenius
f : 𝕎 R
n : ℕ
⊢ coeff (↑frobenius (↑(map ↑(RingEquiv.symm (_root_.frobeniusEquiv R p))) f)) n = coeff f n
[PROOFSTEP]
rw [frobenius_eq_map_frobenius]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
src✝ : 𝕎 R →+* 𝕎 R := frobenius
f : 𝕎 R
n : ℕ
⊢ coeff (↑(map (_root_.frobenius R p)) (↑(map ↑(RingEquiv.symm (_root_.frobeniusEquiv R p))) f)) n = coeff f n
[PROOFSTEP]
exact frobenius_apply_frobeniusEquiv_symm R p _