[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
x : 𝕎 R
k : ℕ
⊢ coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
[PROOFSTEP]
induction' n with n ih generalizing k
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
⊢ coeff (x * ↑Nat.zero) k = ↑(aeval x.coeff) (wittMulN p Nat.zero k)
[PROOFSTEP]
simp only [Nat.zero_eq, Nat.cast_zero, mul_zero, zero_coeff, wittMulN, AlgHom.map_zero, Pi.zero_apply]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ coeff (x * ↑(Nat.succ n)) k = ↑(aeval x.coeff) (wittMulN p (Nat.succ n) k)
[PROOFSTEP]
rw [wittMulN, Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, mul_add, mul_one, aeval_bind₁, add_coeff]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ peval (wittAdd p k) ![(x * ↑n).coeff, x.coeff] =
    ↑(aeval fun i => ↑(aeval x.coeff) (Function.uncurry ![wittMulN p n, X] i)) (wittAdd p k)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] = fun i => ↑(aeval x.coeff) (Function.uncurry ![wittMulN p n, X] i)
[PROOFSTEP]
ext1 ⟨b, i⟩
[GOAL]
case h.mk
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k : ℕ
b : Fin 2
i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] (b, i) = ↑(aeval x.coeff) (Function.uncurry ![wittMulN p n, X] (b, i))
[PROOFSTEP]
fin_cases b
[GOAL]
case h.mk.head
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ({ val := 0, isLt := (_ : 0 < 2) }, i) =
    ↑(aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ({ val := 0, isLt := (_ : 0 < 2) }, i))
[PROOFSTEP]
simp [Function.uncurry, Matrix.cons_val_zero, ih]
[GOAL]
case h.mk.tail.head
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, i) =
    ↑(aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, i))
[PROOFSTEP]
simp [Function.uncurry, Matrix.cons_val_one, Matrix.head_cons, aeval_X]
[GOAL]
p : ℕ
R✝ : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R✝
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
⊢ (x * ↑n).coeff = fun n_1 => ↑(aeval x.coeff) (wittMulN p n n_1)
[PROOFSTEP]
funext k
[GOAL]
case h
p : ℕ
R✝ : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R✝
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
k : ℕ
⊢ coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
[PROOFSTEP]
exact mulN_coeff n x k
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n k : ℕ
⊢ ↑(bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k : ℕ
⊢ ↑(bind₁ (wittMulN p Nat.zero)) (wittPolynomial p ℤ k) = ↑Nat.zero * wittPolynomial p ℤ k
[PROOFSTEP]
simp [wittMulN, Nat.cast_zero, zero_mul, bind₁_zero_wittPolynomial]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k n : ℕ
ih : ↑(bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ ↑(bind₁ (wittMulN p (Nat.succ n))) (wittPolynomial p ℤ k) = ↑(Nat.succ n) * wittPolynomial p ℤ k
[PROOFSTEP]
rw [wittMulN, ← bind₁_bind₁, wittAdd, wittStructureInt_prop]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k n : ℕ
ih : ↑(bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ ↑(bind₁ (Function.uncurry ![wittMulN p n, X]))
      (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (wittPolynomial p ℤ k)) (X 0 + X 1)) =
    ↑(Nat.succ n) * wittPolynomial p ℤ k
[PROOFSTEP]
simp only [AlgHom.map_add, Nat.cast_succ, bind₁_X_right]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k n : ℕ
ih : ↑(bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ ↑(bind₁ (Function.uncurry ![wittMulN p n, X])) (↑(rename (Prod.mk 0)) (wittPolynomial p ℤ k)) +
      ↑(bind₁ (Function.uncurry ![wittMulN p n, X])) (↑(rename (Prod.mk 1)) (wittPolynomial p ℤ k)) =
    (↑n + 1) * wittPolynomial p ℤ k
[PROOFSTEP]
rw [add_mul, one_mul, bind₁_rename, bind₁_rename]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k n : ℕ
ih : ↑(bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ ↑(bind₁ (Function.uncurry ![wittMulN p n, X] ∘ Prod.mk 0)) (wittPolynomial p ℤ k) +
      ↑(bind₁ (Function.uncurry ![wittMulN p n, X] ∘ Prod.mk 1)) (wittPolynomial p ℤ k) =
    ↑n * wittPolynomial p ℤ k + wittPolynomial p ℤ k
[PROOFSTEP]
simp only [ih, Function.uncurry, Function.comp, bind₁_X_left, AlgHom.id_apply, Matrix.cons_val_zero, Matrix.head_cons,
  Matrix.cons_val_one]


[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ degree (succNthDefiningPoly p n a₁ a₂ bs) = ↑p
[PROOFSTEP]
have : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = (p : WithBot ℕ) :=
  by
  rw [degree_mul, degree_C]
  · simp only [Nat.cast_withBot, add_zero, degree_X, degree_pow, Nat.smul_one_eq_coe]
  · exact pow_ne_zero _ ha₁
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1))) = ↑p
[PROOFSTEP]
rw [degree_mul, degree_C]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ degree (X ^ p) + 0 = ↑p
[PROOFSTEP]
simp only [Nat.cast_withBot, add_zero, degree_X, degree_pow, Nat.smul_one_eq_coe]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ coeff a₁ 0 ^ p ^ (n + 1) ≠ 0
[PROOFSTEP]
exact pow_ne_zero _ ha₁
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1))) = ↑p
⊢ degree (succNthDefiningPoly p n a₁ a₂ bs) = ↑p
[PROOFSTEP]
have : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree = (p : WithBot ℕ) :=
  by
  rw [degree_sub_eq_left_of_degree_lt, this]
  rw [this, degree_mul, degree_C, degree_X, add_zero]
  · exact_mod_cast hp.out.one_lt
  · exact pow_ne_zero _ ha₂
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1))) = ↑p
⊢ degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1)) - X * ↑C (coeff a₂ 0 ^ p ^ (n + 1))) = ↑p
[PROOFSTEP]
rw [degree_sub_eq_left_of_degree_lt, this]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1))) = ↑p
⊢ degree (X * ↑C (coeff a₂ 0 ^ p ^ (n + 1))) < degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1)))
[PROOFSTEP]
rw [this, degree_mul, degree_C, degree_X, add_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1))) = ↑p
⊢ 1 < ↑p
[PROOFSTEP]
exact_mod_cast hp.out.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1))) = ↑p
⊢ coeff a₂ 0 ^ p ^ (n + 1) ≠ 0
[PROOFSTEP]
exact pow_ne_zero _ ha₂
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this✝ : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1))) = ↑p
this : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1)) - X * ↑C (coeff a₂ 0 ^ p ^ (n + 1))) = ↑p
⊢ degree (succNthDefiningPoly p n a₁ a₂ bs) = ↑p
[PROOFSTEP]
rw [succNthDefiningPoly, degree_add_eq_left_of_degree_lt, this]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this✝ : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1))) = ↑p
this : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1)) - X * ↑C (coeff a₂ 0 ^ p ^ (n + 1))) = ↑p
⊢ degree
      (↑C
        (coeff a₁ (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
            coeff a₂ (n + 1) * bs 0 ^ p ^ (n + 1) -
          nthRemainder p n bs (truncateFun (n + 1) a₂))) <
    degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1)) - X * ↑C (coeff a₂ 0 ^ p ^ (n + 1)))
[PROOFSTEP]
apply lt_of_le_of_lt degree_C_le
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this✝ : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1))) = ↑p
this : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1)) - X * ↑C (coeff a₂ 0 ^ p ^ (n + 1))) = ↑p
⊢ 0 < degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1)) - X * ↑C (coeff a₂ 0 ^ p ^ (n + 1)))
[PROOFSTEP]
rw [this]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this✝ : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1))) = ↑p
this : degree (X ^ p * ↑C (coeff a₁ 0 ^ p ^ (n + 1)) - X * ↑C (coeff a₂ 0 ^ p ^ (n + 1))) = ↑p
⊢ 0 < ↑p
[PROOFSTEP]
exact_mod_cast hp.out.pos
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ Polynomial.degree (succNthDefiningPoly p n a₁ a₂ bs) ≠ 0
[PROOFSTEP]
simp only [succNthDefiningPoly_degree p n a₁ a₂ bs ha₁ ha₂, ne_eq, Nat.cast_eq_zero, hp.out.ne_zero, not_false_eq_true]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) + coeff a₁ (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ bs ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) + coeff a₂ (n + 1) * bs 0 ^ p ^ (n + 1) +
      nthRemainder p n bs (truncateFun (n + 1) a₂)
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) + coeff a₁ (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) + coeff a₂ (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
[PROOFSTEP]
have := succNthVal_spec p n a₁ a₂ bs ha₁ ha₂
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this : Polynomial.IsRoot (succNthDefiningPoly p n a₁ a₂ bs) (succNthVal p n a₁ a₂ bs ha₁ ha₂)
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) + coeff a₁ (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) + coeff a₂ (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
[PROOFSTEP]
simp only [Polynomial.map_add, Polynomial.eval_X, Polynomial.map_pow, Polynomial.eval_C, Polynomial.eval_pow,
  succNthDefiningPoly, Polynomial.eval_mul, Polynomial.eval_add, Polynomial.eval_sub, Polynomial.map_mul,
  Polynomial.map_sub, Polynomial.IsRoot.def] at this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this :
  succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) +
      (coeff a₁ (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
          coeff a₂ (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) + coeff a₁ (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) + coeff a₂ (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
this :
  succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) +
      (coeff a₁ (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
          coeff a₂ (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) + coeff a₁ (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) + coeff a₂ (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) +
      (coeff a₁ (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
          coeff a₂ (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂))
[PROOFSTEP]
ring
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ solution p a₁ a₂ ≠ 0
[PROOFSTEP]
intro h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
h : solution p a₁ a₂ = 0
⊢ False
[PROOFSTEP]
have := solution_spec p a₁ a₂
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
h : solution p a₁ a₂ = 0
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
⊢ False
[PROOFSTEP]
rw [h, zero_pow] at this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 = coeff a₂ 0 / coeff a₁ 0
⊢ False
[PROOFSTEP]
simpa [ha₁, ha₂] using _root_.div_eq_zero_iff.mp this.symm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
⊢ 0 < p - 1
[PROOFSTEP]
exact tsub_pos_of_lt hp.out.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
⊢ solution p a₁ a₂ ^ p * coeff a₁ 0 = solution p a₁ a₂ * coeff a₂ 0
[PROOFSTEP]
have := solution_spec p a₁ a₂
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
⊢ solution p a₁ a₂ ^ p * coeff a₁ 0 = solution p a₁ a₂ * coeff a₂ 0
[PROOFSTEP]
cases' Nat.exists_eq_succ_of_ne_zero hp.out.ne_zero with q hq
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
⊢ solution p a₁ a₂ ^ p * coeff a₁ 0 = solution p a₁ a₂ * coeff a₂ 0
[PROOFSTEP]
have hq' : q = p - 1 := by simp only [hq, tsub_zero, Nat.succ_sub_succ_eq_sub]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
⊢ q = p - 1
[PROOFSTEP]
simp only [hq, tsub_zero, Nat.succ_sub_succ_eq_sub]
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
⊢ solution p a₁ a₂ ^ p * coeff a₁ 0 = solution p a₁ a₂ * coeff a₂ 0
[PROOFSTEP]
conv_lhs =>
  congr
  congr
  ·skip
  ·rw [hq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| solution p a₁ a₂ ^ p * coeff a₁ 0
[PROOFSTEP]
  congr
  congr
  ·skip
  ·rw [hq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| solution p a₁ a₂ ^ p * coeff a₁ 0
[PROOFSTEP]
  congr
  congr
  ·skip
  ·rw [hq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| solution p a₁ a₂ ^ p * coeff a₁ 0
[PROOFSTEP]
congr
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| solution p a₁ a₂ ^ p
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| coeff a₁ 0
[PROOFSTEP]
congr
[GOAL]
case a.a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| solution p a₁ a₂
case a.a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| p
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| coeff a₁ 0
[PROOFSTEP]
·skip
[GOAL]
case a.a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| solution p a₁ a₂
[PROOFSTEP]
skip
[GOAL]
case a.a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| solution p a₁ a₂
[PROOFSTEP]
skip
[GOAL]
case a.a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| solution p a₁ a₂
[PROOFSTEP]
skip
[GOAL]
case a.a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| p
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| coeff a₁ 0
[PROOFSTEP]
·rw [hq]
[GOAL]
case a.a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| p
[PROOFSTEP]
rw [hq]
[GOAL]
case a.a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| p
[PROOFSTEP]
rw [hq]
[GOAL]
case a.a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
| p
[PROOFSTEP]
rw [hq]
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
⊢ solution p a₁ a₂ ^ Nat.succ q * coeff a₁ 0 = solution p a₁ a₂ * coeff a₂ 0
[PROOFSTEP]
rw [pow_succ', hq', this]
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = coeff a₂ 0 / coeff a₁ 0
q : ℕ
hq : p = Nat.succ q
hq' : q = p - 1
⊢ coeff a₂ 0 / coeff a₁ 0 * solution p a₁ a₂ * coeff a₁ 0 = solution p a₁ a₂ * coeff a₂ 0
[PROOFSTEP]
field_simp [ha₁, mul_comm]
[GOAL]
n : ℕ
i : Fin (n + 1)
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑i) (Nat.succ n)
[PROOFSTEP]
apply Fin.is_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ frobeniusRotation p ha₁ ha₂ ≠ 0
[PROOFSTEP]
intro h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ False
[PROOFSTEP]
apply solution_nonzero p ha₁ ha₂
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ solution p a₁ a₂ = 0
[PROOFSTEP]
simpa [← h, frobeniusRotation, frobeniusRotationCoeff] using WittVector.zero_coeff p k 0
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ ↑frobenius (frobeniusRotation p ha₁ ha₂) * a₁ = frobeniusRotation p ha₁ ha₂ * a₂
[PROOFSTEP]
ext n
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
n : ℕ
⊢ coeff (↑frobenius (frobeniusRotation p ha₁ ha₂) * a₁) n = coeff (frobeniusRotation p ha₁ ha₂ * a₂) n
[PROOFSTEP]
cases' n with n
[GOAL]
case h.zero
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ coeff (↑frobenius (frobeniusRotation p ha₁ ha₂) * a₁) Nat.zero = coeff (frobeniusRotation p ha₁ ha₂ * a₂) Nat.zero
[PROOFSTEP]
simp only [WittVector.mul_coeff_zero, WittVector.coeff_frobenius_charP, frobeniusRotation, frobeniusRotationCoeff,
  Nat.zero_eq]
[GOAL]
case h.zero
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
⊢ coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) 0 ^ p * coeff a₁ 0 =
    coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) 0 * coeff a₂ 0
[PROOFSTEP]
apply solution_spec' _ ha₁
[GOAL]
case h.succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
n : ℕ
⊢ coeff (↑frobenius (frobeniusRotation p ha₁ ha₂) * a₁) (Nat.succ n) =
    coeff (frobeniusRotation p ha₁ ha₂ * a₂) (Nat.succ n)
[PROOFSTEP]
simp only [nthRemainder_spec, WittVector.coeff_frobenius_charP, frobeniusRotationCoeff, frobeniusRotation]
[GOAL]
case h.succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
n : ℕ
⊢ coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) (n + 1) ^ p * coeff a₁ 0 ^ p ^ (n + 1) +
        coeff a₁ (n + 1) * (coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) 0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (↑frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))))
        (truncateFun (n + 1) a₁) =
    coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) (n + 1) * coeff a₂ 0 ^ p ^ (n + 1) +
        coeff a₂ (n + 1) * coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) 0 ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) (truncateFun (n + 1) a₂)
[PROOFSTEP]
have := succNthVal_spec' p n a₁ a₂ (fun i : Fin (n + 1) => frobeniusRotationCoeff p ha₁ ha₂ i.val) ha₁ ha₂
[GOAL]
case h.succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) +
        coeff a₁ (n + 1) * (frobeniusRotationCoeff p ha₁ ha₂ ↑0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v => frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) +
        coeff a₂ (n + 1) * frobeniusRotationCoeff p ha₁ ha₂ ↑0 ^ p ^ (n + 1) +
      nthRemainder p n (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) (truncateFun (n + 1) a₂)
⊢ coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) (n + 1) ^ p * coeff a₁ 0 ^ p ^ (n + 1) +
        coeff a₁ (n + 1) * (coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) 0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (↑frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))))
        (truncateFun (n + 1) a₁) =
    coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) (n + 1) * coeff a₂ 0 ^ p ^ (n + 1) +
        coeff a₂ (n + 1) * coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) 0 ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) (truncateFun (n + 1) a₂)
[PROOFSTEP]
simp only [frobeniusRotationCoeff, Fin.val_zero] at this
[GOAL]
case h.succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) +
        coeff a₁ (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v => frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) +
        coeff a₂ (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) (truncateFun (n + 1) a₂)
⊢ coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) (n + 1) ^ p * coeff a₁ 0 ^ p ^ (n + 1) +
        coeff a₁ (n + 1) * (coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) 0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (↑frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))))
        (truncateFun (n + 1) a₁) =
    coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) (n + 1) * coeff a₂ 0 ^ p ^ (n + 1) +
        coeff a₂ (n + 1) * coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) 0 ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) (truncateFun (n + 1) a₂)
[PROOFSTEP]
convert this using 3
[GOAL]
case h.e'_2.h.e'_6.h.e'_7
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) +
        coeff a₁ (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v => frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) +
        coeff a₂ (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) (truncateFun (n + 1) a₂)
⊢ truncateFun (n + 1) (↑frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))) = fun v =>
    frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p
[PROOFSTEP]
apply TruncatedWittVector.ext
[GOAL]
case h.e'_2.h.e'_6.h.e'_7.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) +
        coeff a₁ (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v => frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) +
        coeff a₂ (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) (truncateFun (n + 1) a₂)
⊢ ∀ (i : Fin (n + 1)),
    TruncatedWittVector.coeff i (truncateFun (n + 1) (↑frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂)))) =
      TruncatedWittVector.coeff i fun v => frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p
[PROOFSTEP]
intro i
[GOAL]
case h.e'_2.h.e'_6.h.e'_7.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) +
        coeff a₁ (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v => frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) +
        coeff a₂ (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) (truncateFun (n + 1) a₂)
i : Fin (n + 1)
⊢ TruncatedWittVector.coeff i (truncateFun (n + 1) (↑frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂)))) =
    TruncatedWittVector.coeff i fun v => frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p
[PROOFSTEP]
simp only [WittVector.coeff_truncateFun, WittVector.coeff_frobenius_charP]
[GOAL]
case h.e'_2.h.e'_6.h.e'_7.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : coeff a₁ 0 ≠ 0
ha₂ : coeff a₂ 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * coeff a₁ 0 ^ p ^ (n + 1) +
        coeff a₁ (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v => frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * coeff a₂ 0 ^ p ^ (n + 1) +
        coeff a₂ (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun i => frobeniusRotationCoeff p ha₁ ha₂ ↑i) (truncateFun (n + 1) a₂)
i : Fin (n + 1)
⊢ coeff (mk p (frobeniusRotationCoeff p ha₁ ha₂)) ↑i ^ p =
    TruncatedWittVector.coeff i fun v => frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
⊢ let b := frobeniusRotation p hr' hq';
  ↑φ (↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) *
      Localization.mk (↑p ^ m * r') { val := ↑p ^ n * q', property := hq } =
    ↑p ^ (↑m - ↑n) * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
[PROOFSTEP]
intro b
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ ↑φ (↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) *
      Localization.mk (↑p ^ m * r') { val := ↑p ^ n * q', property := hq } =
    ↑p ^ (↑m - ↑n) * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
[PROOFSTEP]
have key : WittVector.frobenius b * (p : 𝕎 k) ^ m * r' * (p : 𝕎 k) ^ n = (p : 𝕎 k) ^ m * b * ((p : 𝕎 k) ^ n * q') :=
  by
  have H := congr_arg (fun x : 𝕎 k => x * (p : 𝕎 k) ^ m * (p : 𝕎 k) ^ n) (frobenius_frobeniusRotation p hr' hq')
  dsimp at H
  refine' (Eq.trans _ H).trans _ <;> ring
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
[PROOFSTEP]
have H := congr_arg (fun x : 𝕎 k => x * (p : 𝕎 k) ^ m * (p : 𝕎 k) ^ n) (frobenius_frobeniusRotation p hr' hq')
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
H :
  (fun x => x * ↑p ^ m * ↑p ^ n) (↑frobenius (frobeniusRotation p hr' hq') * r') =
    (fun x => x * ↑p ^ m * ↑p ^ n) (frobeniusRotation p hr' hq' * q')
⊢ ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
[PROOFSTEP]
dsimp at H
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
H : ↑frobenius (frobeniusRotation p hr' hq') * r' * ↑p ^ m * ↑p ^ n = frobeniusRotation p hr' hq' * q' * ↑p ^ m * ↑p ^ n
⊢ ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
[PROOFSTEP]
refine' (Eq.trans _ H).trans _
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
H : ↑frobenius (frobeniusRotation p hr' hq') * r' * ↑p ^ m * ↑p ^ n = frobeniusRotation p hr' hq' * q' * ↑p ^ m * ↑p ^ n
⊢ ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑frobenius (frobeniusRotation p hr' hq') * r' * ↑p ^ m * ↑p ^ n
[PROOFSTEP]
ring
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
H : ↑frobenius (frobeniusRotation p hr' hq') * r' * ↑p ^ m * ↑p ^ n = frobeniusRotation p hr' hq' * q' * ↑p ^ m * ↑p ^ n
⊢ frobeniusRotation p hr' hq' * q' * ↑p ^ m * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
[PROOFSTEP]
ring
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
⊢ ↑φ (↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) *
      Localization.mk (↑p ^ m * r') { val := ↑p ^ n * q', property := hq } =
    ↑p ^ (↑m - ↑n) * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
[PROOFSTEP]
have hq'' : algebraMap (𝕎 k) (FractionRing (𝕎 k)) q' ≠ 0 :=
  by
  have hq''' : q' ≠ 0 := fun h => hq' (by simp [h])
  simpa only [Ne.def, map_zero] using (IsFractionRing.injective (𝕎 k) (FractionRing (𝕎 k))).ne hq'''
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
⊢ ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
[PROOFSTEP]
have hq''' : q' ≠ 0 := fun h => hq' (by simp [h])
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
h : q' = 0
⊢ coeff q' 0 = 0
[PROOFSTEP]
simp [h]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
hq''' : q' ≠ 0
⊢ ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
[PROOFSTEP]
simpa only [Ne.def, map_zero] using (IsFractionRing.injective (𝕎 k) (FractionRing (𝕎 k))).ne hq'''
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
hq'' : ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ ↑φ (↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) *
      Localization.mk (↑p ^ m * r') { val := ↑p ^ n * q', property := hq } =
    ↑p ^ (↑m - ↑n) * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
[PROOFSTEP]
rw [zpow_sub₀ (FractionRing.p_nonzero p k)]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
hq'' : ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ ↑φ (↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) *
      Localization.mk (↑p ^ m * r') { val := ↑p ^ n * q', property := hq } =
    ↑p ^ ↑m / ↑p ^ ↑n * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
[PROOFSTEP]
field_simp [FractionRing.p_nonzero p k]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
hq'' : ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ ↑φ (↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) (frobeniusRotation p hr' hq')) *
        (↑p ^ m * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) r') *
      ↑p ^ n =
    ↑p ^ m * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) (frobeniusRotation p hr' hq') *
      (↑p ^ n * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q')
[PROOFSTEP]
simp only [IsFractionRing.fieldEquivOfRingEquiv, IsLocalization.ringEquivOfRingEquiv_eq, RingEquiv.coe_ofBijective]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
hq'' : ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ ↑(algebraMap (𝕎 k) (Localization (nonZeroDivisors (𝕎 k)))) (↑(frobeniusEquiv p k) (frobeniusRotation p hr' hq')) *
        (↑p ^ m * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) r') *
      ↑p ^ n =
    ↑p ^ m * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) (frobeniusRotation p hr' hq') *
      (↑p ^ n * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q')
[PROOFSTEP]
convert congr_arg (fun x => algebraMap (𝕎 k) (FractionRing (𝕎 k)) x) key using 1
[GOAL]
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
hq'' : ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ ↑(algebraMap (𝕎 k) (Localization (nonZeroDivisors (𝕎 k)))) (↑(frobeniusEquiv p k) (frobeniusRotation p hr' hq')) *
        (↑p ^ m * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) r') *
      ↑p ^ n =
    ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) (↑frobenius b * ↑p ^ m * r' * ↑p ^ n)
[PROOFSTEP]
simp only [RingHom.map_mul, RingHom.map_pow, map_natCast, frobeniusEquiv_apply]
[GOAL]
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
hq'' : ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ ↑(algebraMap (𝕎 k) (Localization (nonZeroDivisors (𝕎 k)))) (↑frobenius (frobeniusRotation p hr' hq')) *
        (↑p ^ m * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) r') *
      ↑p ^ n =
    ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) (↑frobenius (frobeniusRotation p hr' hq')) * ↑p ^ m *
        ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) r' *
      ↑p ^ n
[PROOFSTEP]
ring
[GOAL]
case h.e'_3
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : ↑frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
hq'' : ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ ↑p ^ m * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) (frobeniusRotation p hr' hq') *
      (↑p ^ n * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q') =
    ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) (↑p ^ m * b * (↑p ^ n * q'))
[PROOFSTEP]
simp only [RingHom.map_mul, RingHom.map_pow, map_natCast]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
ha : a ≠ 0
⊢ ∃ b hb m, ↑φ b * a = ↑p ^ m * b
[PROOFSTEP]
revert ha
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
⊢ a ≠ 0 → ∃ b hb m, ↑φ b * a = ↑p ^ m * b
[PROOFSTEP]
refine' Localization.induction_on a _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
⊢ ∀ (y : 𝕎 k × { x // x ∈ nonZeroDivisors (𝕎 k) }),
    Localization.mk y.fst y.snd ≠ 0 → ∃ b hb m, ↑φ b * Localization.mk y.fst y.snd = ↑p ^ m * b
[PROOFSTEP]
rintro ⟨r, q, hq⟩ hrq
[GOAL]
case mk.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, { val := q, property := hq }).fst (r, { val := q, property := hq }).snd ≠ 0
⊢ ∃ b hb m,
    ↑φ b * Localization.mk (r, { val := q, property := hq }).fst (r, { val := q, property := hq }).snd = ↑p ^ m * b
[PROOFSTEP]
have hq0 : q ≠ 0 := mem_nonZeroDivisors_iff_ne_zero.1 hq
[GOAL]
case mk.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, { val := q, property := hq }).fst (r, { val := q, property := hq }).snd ≠ 0
hq0 : q ≠ 0
⊢ ∃ b hb m,
    ↑φ b * Localization.mk (r, { val := q, property := hq }).fst (r, { val := q, property := hq }).snd = ↑p ^ m * b
[PROOFSTEP]
have hr0 : r ≠ 0 := fun h => hrq (by simp [h])
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, { val := q, property := hq }).fst (r, { val := q, property := hq }).snd ≠ 0
hq0 : q ≠ 0
h : r = 0
⊢ Localization.mk (r, { val := q, property := hq }).fst (r, { val := q, property := hq }).snd = 0
[PROOFSTEP]
simp [h]
[GOAL]
case mk.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, { val := q, property := hq }).fst (r, { val := q, property := hq }).snd ≠ 0
hq0 : q ≠ 0
hr0 : r ≠ 0
⊢ ∃ b hb m,
    ↑φ b * Localization.mk (r, { val := q, property := hq }).fst (r, { val := q, property := hq }).snd = ↑p ^ m * b
[PROOFSTEP]
obtain ⟨m, r', hr', rfl⟩ := exists_eq_pow_p_mul r hr0
[GOAL]
case mk.mk.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hq0 : q ≠ 0
m : ℕ
r' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hrq :
  Localization.mk (↑p ^ m * r', { val := q, property := hq }).fst (↑p ^ m * r', { val := q, property := hq }).snd ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
⊢ ∃ b hb m_1,
    ↑φ b *
        Localization.mk (↑p ^ m * r', { val := q, property := hq }).fst
          (↑p ^ m * r', { val := q, property := hq }).snd =
      ↑p ^ m_1 * b
[PROOFSTEP]
obtain ⟨n, q', hq', rfl⟩ := exists_eq_pow_p_mul q hq0
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq :
  Localization.mk (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).fst
      (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).snd ≠
    0
⊢ ∃ b hb m_1,
    ↑φ b *
        Localization.mk (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).fst
          (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).snd =
      ↑p ^ m_1 * b
[PROOFSTEP]
let b := frobeniusRotation p hr' hq'
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq :
  Localization.mk (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).fst
      (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).snd ≠
    0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ ∃ b hb m_1,
    ↑φ b *
        Localization.mk (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).fst
          (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).snd =
      ↑p ^ m_1 * b
[PROOFSTEP]
refine' ⟨algebraMap (𝕎 k) (FractionRing (𝕎 k)) b, _, m - n, _⟩
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro.refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq :
  Localization.mk (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).fst
      (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).snd ≠
    0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b ≠ 0
[PROOFSTEP]
simpa only [map_zero] using
  (IsFractionRing.injective (WittVector p k) (FractionRing (WittVector p k))).ne (frobeniusRotation_nonzero p hr' hq')
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro.refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : coeff r' 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : coeff q' 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq :
  Localization.mk (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).fst
      (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).snd ≠
    0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ ↑φ (↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) *
      Localization.mk (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).fst
        (↑p ^ m * r', { val := ↑p ^ n * q', property := hq }).snd =
    ↑p ^ (↑m - ↑n) * ↑(algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
[PROOFSTEP]
exact exists_frobenius_solution_fractionRing_aux p m n r' q' hr' hq' hq