awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
      nthRemainder p n bs (truncateFun (n + 1) a₂)
have rw : succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
    (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
      nthRemainder p n bs (truncateFun (n + 1) a₂)) =
  0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
have this : Polynomial.IsRoot (succNthDefiningPoly p n a₁ a₂ bs) (succNthVal p n a₁ a₂ bs ha₁ ha₂)
Tactic: have := succNthVal_spec p n a₁ a₂ bs ha₁ ha₂
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 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 * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
have this₁ : succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
      succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
    (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
          nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
        a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
      nthRemainder p n bs (truncateFun (n + 1) a₂)) =
  0
Tactic: simp only [Polynomial.eval_X, Polynomial.eval_C,
    Polynomial.eval_pow, succNthDefiningPoly, Polynomial.eval_mul, Polynomial.eval_add,
    Polynomial.eval_sub, Polynomial.IsRoot.def]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
            nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (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 * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
have h : succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
    (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
      nthRemainder p n bs (truncateFun (n + 1) a₂)) =
  succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
      succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
    (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
          nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
        a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
      nthRemainder p n bs (truncateFun (n + 1) a₂))
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
⊢ False
have this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
Tactic: have := solution_spec p a₁ a₂
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ False
have rw : ∀ (this : 0 = a₂.coeff 0 / a₁.coeff 0), False
Tactic: rw [h, zero_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
rw : ∀ (this : 0 = a₂.coeff 0 / a₁.coeff 0), False
⊢ False
have rw₁ : ∀ (this : HPow.hPow (α := k) 0 (p - 1) = a₂.coeff 0 / a₁.coeff 0), p - 1 ≠ 0
Tactic: rw [h, zero_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
have this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
Tactic: have := solution_spec p a₁ a₂
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
have this₁ : ∃ (k : ℕ), p = k.succ
Tactic: have := Nat.exists_eq_succ_of_ne_zero hp.out.ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ False
have apply : solution p a₁ a₂ = 0
Tactic: apply solution_nonzero p ha₁ ha₂
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁ =
    frobeniusRotation p ha₁ ha₂ * a₂
have h : ∀ (n : ℕ),
  (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff n =
    (frobeniusRotation p ha₁ ha₂ * a₂).coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff n =
    (frobeniusRotation p ha₁ ha₂ * a₂).coeff n
have h : (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff 0 =
  (frobeniusRotation p ha₁ ha₂ * a₂).coeff 0
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
h :
  (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff 0 =
    (frobeniusRotation p ha₁ ha₂ * a₂).coeff 0
⊢ (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff n =
    (frobeniusRotation p ha₁ ha₂ * a₂).coeff n
have h₁ : ∀ (n : ℕ),
  (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff (n + 1) =
    (frobeniusRotation p ha₁ ha₂ * a₂).coeff (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff 0 =
    (frobeniusRotation p ha₁ ha₂ * a₂).coeff 0
have h : solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
Tactic: simp only [WittVector.mul_coeff_zero, WittVector.coeff_frobenius_charP, frobeniusRotation,
      coeff_mk, frobeniusRotationCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff (n + 1) =
    (frobeniusRotation p ha₁ ha₂ * a₂).coeff (n + 1)
have h : succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ ^ p *
        a₁.coeff 0 ^ p ^ (n + 1) +
      a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
    nthRemainder p n (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂))))
      (truncateFun (n + 1) a₁) =
  succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ *
        a₂.coeff 0 ^ p ^ (n + 1) +
      a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
    nthRemainder p n (truncateFun (n + 1) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) (truncateFun (n + 1) a₂)
Tactic: simp only [nthRemainder_spec, WittVector.coeff_frobenius_charP,
      frobeniusRotation, coeff_mk, frobeniusRotationCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ ^ p *
          a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂))))
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ *
          a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) (truncateFun (n + 1) a₂)
have this : succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ ^ p *
        a₁.coeff 0 ^ p ^ (n + 1) +
      a₁.coeff (n + 1) * (frobeniusRotationCoeff p ha₁ ha₂ (↑0 : ℕ) ^ p) ^ p ^ (n + 1) +
    nthRemainder p n (fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p) (truncateFun (n + 1) a₁) =
  succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ *
        a₂.coeff 0 ^ p ^ (n + 1) +
      a₂.coeff (n + 1) * frobeniusRotationCoeff p ha₁ ha₂ (↑0 : ℕ) ^ p ^ (n + 1) +
    nthRemainder p n (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) (truncateFun (n + 1) a₂)
Tactic: have :=
      succNthVal_spec' p n a₁ a₂ (fun i : Fin (n + 1) => frobeniusRotationCoeff p ha₁ ha₂ i.val)
        ha₁ ha₂
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ ^ p *
          a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p)
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ *
          a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) (truncateFun (n + 1) a₂)
⊢ succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ ^ p *
          a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂))))
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ *
          a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) (truncateFun (n + 1) a₂)
have h : Eq.{u_1 + 1} (α := Fin (n + 1) → k)
  (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) :
    TruncatedWittVector p (n + 1) k)
  fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p
Tactic: convert! this using 3
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ Eq.{u_1 + 1} (α := Fin (n + 1) → k)
    (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) :
      TruncatedWittVector p (n + 1) k)
    fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p
have h : ∀ (i : Fin (n + 1)),
  Eq.{u_1 + 1} (α := k)
    (TruncatedWittVector.coeff (p := p) i
      (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂)))))
    (TruncatedWittVector.coeff (p := p) i fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p)
Tactic: apply TruncatedWittVector.ext
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
i : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := k)
    (TruncatedWittVector.coeff (p := p) i
      (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂)))))
    (TruncatedWittVector.coeff (p := p) i fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p)
have h : (mk p (frobeniusRotationCoeff p ha₁ ha₂)).coeff (↑i : ℕ) ^ p =
  TruncatedWittVector.coeff (p := p) i fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p
Tactic: simp only [WittVector.coeff_truncateFun, WittVector.coeff_frobenius_charP]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k)) (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q')
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
            (a : FractionRing (𝕎 k)) → Localization (nonZeroDivisors (𝕎 k)))
          ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b) :
        Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      (Localization.mk (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r')
        (Subtype.mk (p := fun (x : 𝕎 k) ↦
          Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
          (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq)) =
    HMul.hMul (β := FractionRing (𝕎 k))
      (HPow.hPow (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (↑p : Localization (nonZeroDivisors (𝕎 k)))
        (HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))
have key : HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r' = q' * b
Tactic: have key : WittVector.frobenius b * r' = q' * b := by
    linear_combination frobenius_frobeniusRotation p hr' hq'
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k)) (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q')
b : 𝕎 k := frobeniusRotation p hr' hq'
key : HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r' = q' * b
⊢ Ne (α := FractionRing (𝕎 k))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
    (0 : FractionRing (𝕎 k))
have hq''' : q' ≠ 0
Tactic: have hq''' : q' ≠ 0 := fun h => hq' (by simp [h])
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k)) (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q')
b : 𝕎 k := frobeniusRotation p hr' hq'
key : HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r' = q' * b
⊢ HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
            (a : FractionRing (𝕎 k)) → Localization (nonZeroDivisors (𝕎 k)))
          ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b) :
        Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      (Localization.mk (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r')
        (Subtype.mk (p := fun (x : 𝕎 k) ↦
          Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
          (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq)) =
    HMul.hMul (β := FractionRing (𝕎 k))
      (HPow.hPow (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (↑p : Localization (nonZeroDivisors (𝕎 k)))
        (HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))
have hq'' : Ne (α := FractionRing (𝕎 k))
  ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
  (0 : FractionRing (𝕎 k))
Tactic: have hq'' : algebraMap (𝕎 k) (FractionRing (𝕎 k)) q' ≠ 0 := by
    have hq''' : q' ≠ 0 := fun h => hq' (by simp [h])
    simpa only [Ne, map_zero] using
      (IsFractionRing.injective (𝕎 k) (FractionRing (𝕎 k))).ne hq'''
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k)) (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q')
b : 𝕎 k := frobeniusRotation p hr' hq'
key : HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r' = q' * b
hq'' :
  Ne (α := FractionRing (𝕎 k))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
    (0 : FractionRing (𝕎 k))
⊢ HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
            (a : FractionRing (𝕎 k)) → Localization (nonZeroDivisors (𝕎 k)))
          ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b) :
        Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      (Localization.mk (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r')
        (Subtype.mk (p := fun (x : 𝕎 k) ↦
          Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
          (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq)) =
    HMul.hMul (β := FractionRing (𝕎 k))
      (HPow.hPow (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (↑p : Localization (nonZeroDivisors (𝕎 k)))
        (HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))
have rw : HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
    ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
          (a : FractionRing (𝕎 k)) → Localization (nonZeroDivisors (𝕎 k)))
        ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b) :
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
    (Localization.mk (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r')
      (Subtype.mk (p := fun (x : 𝕎 k) ↦
        Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
        (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq)) =
  HMul.hMul (β := FractionRing (𝕎 k))
    (HPow.hPow (α := FractionRing (𝕎 k)) (β := ℤ) (↑p : FractionRing (𝕎 k)) (↑m : ℤ) /
      HPow.hPow (α := FractionRing (𝕎 k)) (β := ℤ) (↑p : FractionRing (𝕎 k)) (↑n : ℤ))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))
Tactic: rw [zpow_sub₀ (FractionRing.p_nonzero p k)]