awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
rw :
  Eq (α := R)
    (coeff
        (mk p fun (n : ℕ) ↦
          ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n))
        n :
      R)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) : R)
⊢ x.frobeniusFun.coeff n =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n)
have rw₁ : Eq (α := R) (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) : R)
  (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) : R)
Tactic: rw [frobeniusFun, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
R_1 : Type u_2
inst_1 : CommRing R_1
x : 𝕎 R_1
⊢ x.frobeniusFun.coeff = fun (n : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (frobeniusPoly p n)
have h : ∀ (n : ℕ),
  x.frobeniusFun.coeff n =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (frobeniusPoly p n)
Tactic: funext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (frobeniusFun 1) 1
have frobeniusFun_isPoly : ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
  Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (((fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) ∘ fun (x : 𝕎 R) ↦ 1) x) : R)
    ((ghostComponent n : (a : 𝕎 R) → R) (((fun (x : 𝕎 R) ↦ 1) ∘ fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) x) : R)
Tactic: refine
      IsPoly.ext (IsPoly.comp (hg := frobeniusFun_isPoly p) (hf := WittVector.oneIsPoly))
        (IsPoly.comp (hg := WittVector.oneIsPoly) (hf := frobeniusFun_isPoly p)) ?_ _ 0
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (((fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) ∘ fun (x : 𝕎 R) ↦ 1) x) : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (((fun (x : 𝕎 R) ↦ 1) ∘ fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) x) : R)
have simp : ∀ (R : Type u_1) [_Rcr : CommRing R] (n : ℕ),
  Eq.{u_1 + 1} (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (frobeniusFun 1) : R) (1 : R)
Tactic: simp only [Function.comp_apply, map_one, forall_const]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ ∀ (x y : 𝕎 R), (x * y).frobeniusFun = x.frobeniusFun * y.frobeniusFun
have refine_3 : ∀ (R : Type u_1) [R._inst : CommRing R] (x y : 𝕎 R) (n : ℕ),
  Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x * y).frobeniusFun : R)
    ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun * y.frobeniusFun) : R)
Tactic: ghost_calc _ _
Cleared hypotheses: R, inst
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (frobeniusFun 0) 0
have refine : ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
  Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (((fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) ∘ fun (x : 𝕎 R) ↦ 0) x) : R)
    ((ghostComponent n : (a : 𝕎 R) → R) (((fun (x : 𝕎 R) ↦ 0) ∘ fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) x) : R)
Tactic: refine IsPoly.ext (IsPoly.comp (hg := frobeniusFun_isPoly p) (hf := WittVector.zeroIsPoly))
      (IsPoly.comp (hg := WittVector.zeroIsPoly) (hf := frobeniusFun_isPoly p))
      ?_ _ 0
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (((fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) ∘ fun (x : 𝕎 R) ↦ 0) x) : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (((fun (x : 𝕎 R) ↦ 0) ∘ fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) x) : R)
have simp : ∀ (R : Type u_1) [_Rcr : CommRing R] (n : ℕ),
  Eq.{u_1 + 1} (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (frobeniusFun 0) : R) (0 : R)
Tactic: simp only [Function.comp_apply, map_zero, forall_const]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ ∀ (x y : 𝕎 R), (x + y).frobeniusFun = x.frobeniusFun + y.frobeniusFun
have refine_3 : ∀ (R : Type u_1) [R._inst : CommRing R] (x y : 𝕎 R) (n : ℕ),
  Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x + y).frobeniusFun : R)
    ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun + y.frobeniusFun) : R)
Tactic: ghost_calc _ _
Cleared hypotheses: R, inst
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
⊢ coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) x) n = x.coeff n ^ p
have rw : ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) = x.coeff n ^ p
Tactic: rw [coeff_frobenius]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) = x.coeff n ^ p
have calc_1 : Eq.{u_1 + 1} (α := R)
  (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (k : ℕ) ↦ x.coeff k : MvPolynomial ℕ ℤ →ₐ[ℤ] R) :
        (a : MvPolynomial ℕ ℤ) → R)
      (frobeniusPoly p n) :
    R)
  ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
          (frobeniusPoly p n) :
        MvPolynomial ℕ (ZMod p)) :
    R)
Tactic: 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 := ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
calc_1 :
  Eq.{u_1 + 1} (α := R)
    (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (k : ℕ) ↦ x.coeff k : MvPolynomial ℕ ℤ →ₐ[ℤ] R) :
          (a : MvPolynomial ℕ ℤ) → R)
        (frobeniusPoly p n) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPoly p n) :
          MvPolynomial ℕ (ZMod p)) :
      R)
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) = x.coeff n ^ p
have calc_2 : Eq.{u_1 + 1} (α := R)
  ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
          (frobeniusPoly p n) :
        MvPolynomial ℕ (ZMod p)) :
    R)
  ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) :
    R)
Tactic: 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 := ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
calc_1 :
  Eq.{u_1 + 1} (α := R)
    (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (k : ℕ) ↦ x.coeff k : MvPolynomial ℕ ℤ →ₐ[ℤ] R) :
          (a : MvPolynomial ℕ ℤ) → R)
        (frobeniusPoly p n) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPoly p n) :
          MvPolynomial ℕ (ZMod p)) :
      R)
calc_2 :
  Eq.{u_1 + 1} (α := R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPoly p n) :
          MvPolynomial ℕ (ZMod p)) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) :
      R)
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) = x.coeff n ^ p
have calc_3 : (aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R) (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) =
  x.coeff n ^ p
Tactic: 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 := ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
| ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
          (frobeniusPoly p n) :
        MvPolynomial ℕ (ZMod p)) :
    R)
have rw : ((eval₂Hom
        (@RingHom.comp _ (ZMod p) _ _ Semiring.toNonAssocSemiring _ (algebraMap (ZMod p) R) (Int.castRingHom (ZMod p)))
        fun (k : ℕ) ↦ x.coeff k :
      (a : MvPolynomial ℕ ℤ) → R)
    (frobeniusPoly p n) :
  R)
Tactic: rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ Eq.{u_1 + 1} (α := R)
    (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (k : ℕ) ↦ x.coeff k : MvPolynomial ℕ ℤ →ₐ[ℤ] R) :
          (a : MvPolynomial ℕ ℤ) → R)
        (frobeniusPoly p n) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPoly p n) :
          MvPolynomial ℕ (ZMod p)) :
      R)
have calc_1 : Eq (α := R)
  (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (k : ℕ) ↦ x.coeff k : MvPolynomial ℕ ℤ →ₐ[ℤ] R) :
        (a : MvPolynomial ℕ ℤ) → R)
      (frobeniusPoly p n) :
    R)
  ((eval₂Hom
          (@RingHom.comp _ (ZMod p) _ _ Semiring.toNonAssocSemiring _ (algebraMap (ZMod p) R)
            (Int.castRingHom (ZMod p)))
          fun (k : ℕ) ↦ x.coeff k :
        (a : MvPolynomial ℕ ℤ) → R)
      (frobeniusPoly p n) :
    R)
Tactic: conv_rhs => rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ Eq.{u_1 + 1} (α := R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPoly p n) :
          MvPolynomial ℕ (ZMod p)) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) :
      R)
have calc_2 : Eq.{u_1 + 1} (α := R)
  ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) :
    R)
  ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) :
    R)
Tactic: rw [frobeniusPoly_zmod]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) =
    x.coeff n ^ p
have calc_3 : HPow.hPow (α := R) ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R) (X n) : R) p = x.coeff n ^ p
Tactic: rw [map_pow, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
calc_3 :
  HPow.hPow (α := R) ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R) (X n) : R) p = x.coeff n ^ p
⊢ (aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) =
    x.coeff n ^ p
have calc_3₁ : x.coeff n ^ p = x.coeff n ^ p
Tactic: rw [map_pow, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
⊢ Eq (α := 𝕎 R →+* 𝕎 R) frobenius (map (_root_.frobenius R p))
have a : ∀ (x : 𝕎 R) (n : ℕ),
  Eq.{u_1 + 1} (α := R) (coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) x) n)
    (coeff (p := p) ((map (_root_.frobenius R p) : (a : 𝕎 R) → 𝕎 R) x) n)
Tactic: ext (x n)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
f : 𝕎 R
n : ℕ
⊢ coeff (p := p)
      ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R)
        ((frobenius : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
      n =
    f.coeff n
have rw : coeff (p := p)
    ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R)
      ((map (_root_.frobenius R p) : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
    n =
  f.coeff n
Tactic: rw [frobenius_eq_map_frobenius]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
f : 𝕎 R
n : ℕ
⊢ coeff (p := p)
      ((frobenius : (a : 𝕎 R) → 𝕎 R)
        ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
      n =
    f.coeff n
have rw : coeff (p := p)
    ((map (_root_.frobenius R p) : (a : 𝕎 R) → 𝕎 R)
      ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
    n =
  f.coeff n
Tactic: rw [frobenius_eq_map_frobenius]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
have rw : (HPow.hPow (α := k[X]) X p).degree + 0 = (↑p : WithBot ℕ)
Tactic: rw [degree_mul, degree_C]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
rw : (HPow.hPow (α := k[X]) X p).degree + 0 = (↑p : WithBot ℕ)
⊢ (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
have rw₁ : a₁.coeff 0 ^ p ^ (n + 1) ≠ 0
Tactic: rw [degree_mul, degree_C]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ degree (succNthDefiningPoly p n a₁ a₂ bs) = (↑p : WithBot ℕ)
have this : (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
  (↑p : WithBot ℕ)
Tactic: have : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = (p : WithBot ℕ) := by
    rw [degree_mul, degree_C]
    · simp
    · exact pow_ne_zero _ ha₁
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
have rw : (HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree <
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree
Tactic: rw [degree_sub_eq_left_of_degree_lt, this]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ (HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree <
    (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree
have rw : LT.lt (α := WithBot ℕ) 1 (↑p : WithBot ℕ)
Tactic: rw [this, degree_mul, degree_C, degree_X, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
rw : LT.lt (α := WithBot ℕ) 1 (↑p : WithBot ℕ)
⊢ (HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree <
    (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree
have rw₁ : a₂.coeff 0 ^ p ^ (n + 1) ≠ 0
Tactic: rw [this, degree_mul, degree_C, degree_X, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ degree (succNthDefiningPoly p n a₁ a₂ bs) = (↑p : WithBot ℕ)
have this₁ : (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
      HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
  (↑p : WithBot ℕ)
Tactic: 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₂
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this_1 :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ degree (succNthDefiningPoly p n a₁ a₂ bs) = (↑p : WithBot ℕ)
have rw : degree.{u_1} (R := k)
    ((C : (a : k) → k[X])
      (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₂))) <
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
      HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree
Tactic: rw [succNthDefiningPoly, degree_add_eq_left_of_degree_lt, this]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this_1 :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ degree.{u_1} (R := k)
      ((C : (a : k) → k[X])
        (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₂))) <
    (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree
have apply : 0 <
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
      HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree
Tactic: apply lt_of_le_of_lt degree_C_le
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this_1 :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ 0 <
    (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree
have rw : LT.lt (α := WithBot ℕ) 0 (↑p : WithBot ℕ)
Tactic: rw [this]