awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
g : (x : ℕ) → R := fun (x : ℕ) ↦ 0
⊢ x.coeff i =
    (HMul.hMul (α := 𝕎 R)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R)
            (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)).coeff
        i +
      ∑ x_1 ∈ Finset.Iic n \ {i},
        (HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) x_1 : (a : R) → R)
                      (x.coeff x_1) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) x_1)).coeff
          i
have rw : x.coeff i =
  (HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)).coeff
      i +
    (Finset.Iic n \ {i}).sum g
Tactic: rw [Finset.sum_congr rfl (g := g)]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
g : (x : ℕ) → R := fun (x : ℕ) ↦ 0
rw :
  x.coeff i =
    (HMul.hMul (α := 𝕎 R)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R)
            (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)).coeff
        i +
      (Finset.Iic n \ {i}).sum g
⊢ x.coeff i =
    (HMul.hMul (α := 𝕎 R)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R)
            (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)).coeff
        i +
      ∑ x_1 ∈ Finset.Iic n \ {i},
        (HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) x_1 : (a : R) → R)
                      (x.coeff x_1) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) x_1)).coeff
          i
have rw₁ : ∀ x_1 ∈ Finset.Iic n \ {i},
  (HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) x_1 : (a : R) → R) (x.coeff x_1) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) x_1)).coeff
      i =
    g x_1
Tactic: rw [Finset.sum_congr rfl (g := g)]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
g : (x : ℕ) → R := fun (x : ℕ) ↦ 0
b : ℕ
hb : b ∈ Finset.Iic n \ {i}
⊢ (HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) b : (a : R) → R) (x.coeff b) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) b)).coeff
      i =
    g b
have hb₁ : b ≤ n ∧ ¬b = i
Tactic: simp only [Finset.mem_sdiff, Finset.mem_Iic, Finset.mem_singleton] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
x : 𝕎 R
n_1 i : ℕ
hi : i < n_1 + 1
n : ℕ
x_1 x_2 :
  (↑{r : ℕ |
        r ∈ Finset.Iic n_1 ∧
          (HMul.hMul (α := 𝕎 R)
                  ((teichmuller p : (a : R) → 𝕎 R)
                      ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) r : (a : R) → R)
                          (x.coeff r) :
                        R) :
                    𝕎 R)
                  (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) r)).coeff
              n ≠
            0} :
    Type)
a : ℕ
left : a ∈ Finset.Iic n_1
ha :
  (HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) a : (a : R) → R) (x.coeff a) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) a)).coeff
      n ≠
    0
b : ℕ
left_1 : b ∈ Finset.Iic n_1
hb :
  (HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) b : (a : R) → R) (x.coeff b) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) b)).coeff
      n ≠
    0
⊢ (↑(Subtype.mk (p := fun (x_3 : ℕ) ↦
          Membership.mem (γ := Set ℕ)
            {r : ℕ |
              r ∈ Finset.Iic n_1 ∧
                (HMul.hMul (α := 𝕎 R)
                        ((teichmuller p : (a : R) → 𝕎 R)
                            ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) r : (a : R) → R)
                                (x.coeff r) :
                              R) :
                          𝕎 R)
                        (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) r)).coeff
                    n ≠
                  0}
            x_3)
          a ⋯) :
      ℕ) =
    (↑(Subtype.mk (p := fun (x_3 : ℕ) ↦
          Membership.mem (γ := Set ℕ)
            {r : ℕ |
              r ∈ Finset.Iic n_1 ∧
                (HMul.hMul (α := 𝕎 R)
                        ((teichmuller p : (a : R) → 𝕎 R)
                            ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) r : (a : R) → R)
                                (x.coeff r) :
                              R) :
                          𝕎 R)
                        (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) r)).coeff
                    n ≠
                  0}
            x_3)
          b ⋯) :
      ℕ)
have h : a = b
Tactic: dsimp only [ne_eq, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
x : 𝕎 R
n_1 i : ℕ
hi : i < n_1 + 1
n : ℕ
x_1 x_2 :
  (↑{r : ℕ |
        r ∈ Finset.Iic n_1 ∧
          (HMul.hMul (α := 𝕎 R)
                  ((teichmuller p : (a : R) → 𝕎 R)
                      ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) r : (a : R) → R)
                          (x.coeff r) :
                        R) :
                    𝕎 R)
                  (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) r)).coeff
              n ≠
            0} :
    Type)
a : ℕ
left : a ∈ Finset.Iic n_1
ha :
  (HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) a : (a : R) → R) (x.coeff a) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) a)).coeff
      n ≠
    0
b : ℕ
left_1 : b ∈ Finset.Iic n_1
hb :
  (HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) b : (a : R) → R) (x.coeff b) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) b)).coeff
      n ≠
    0
⊢ a = b
have h : n = b
Tactic: rw [← Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) ha]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
S : Type u_2
inst_3 : CommRing S
f g : RingHom.{u_1, u_2} (𝕎 R) S
hp : IsNilpotent.{u_2} (R := S) (↑p : S)
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
      ((g : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
⊢ f = g
have obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := S) (↑p : S) n = 0), f = g
Tactic: obtain ⟨n, hn⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
S : Type u_2
inst_3 : CommRing S
f g : RingHom.{u_1, u_2} (𝕎 R) S
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
      ((g : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
n : ℕ
hn : HPow.hPow (α := S) (↑p : S) n = 0
⊢ f = g
have a : ∀ (x : 𝕎 R), Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) x : S) ((g : (a : 𝕎 R) → S) x : S)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
S : Type u_2
inst_3 : CommRing S
f g : RingHom.{u_1, u_2} (𝕎 R) S
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
      ((g : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
n : ℕ
hn : HPow.hPow (α := S) (↑p : S) n = 0
x : 𝕎 R
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) x : S) ((g : (a : 𝕎 R) → S) x : S)
have a : ∀ (c : 𝕎 R)
  (hc :
    x -
        ∑ i ∈ Finset.Iic n,
          HMul.hMul (α := 𝕎 R)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R)
            (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) =
      HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c),
  Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) x : S) ((g : (a : 𝕎 R) → S) x : S)
Tactic: obtain ⟨c, hc⟩ := (dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff x n)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
S : Type u_2
inst_3 : CommRing S
f g : RingHom.{u_1, u_2} (𝕎 R) S
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
      ((g : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
n : ℕ
hn : HPow.hPow (α := S) (↑p : S) n = 0
x c : 𝕎 R
hc :
  x -
      ∑ i ∈ Finset.Iic n,
        HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) =
    HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c
⊢ HAdd.hAdd (α := S) (β := S)
      ((f : (a : 𝕎 R) → S)
          (x -
            ∑ i ∈ Finset.Iic n,
              HMul.hMul (α := 𝕎 R)
                ((teichmuller p : (a : R) → 𝕎 R)
                    ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R)
                        (x.coeff i) :
                      R) :
                  𝕎 R)
                (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S)
      ((f : (a : 𝕎 R) → S)
          (∑ i ∈ Finset.Iic n,
            HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S) =
    ∑ i ∈ Finset.Iic n,
      HMul.hMul (α := S)
        ((f : (a : 𝕎 R) → S)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R) :
          S)
        (HPow.hPow (α := S) (↑p : S) i)
have rw : HAdd.hAdd (α := S) (β := S) ((f : (a : 𝕎 R) → S) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c) : S)
    ((f : (a : 𝕎 R) → S)
        (∑ i ∈ Finset.Iic n,
          HMul.hMul (α := 𝕎 R)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R)
            (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
      S) =
  ∑ i ∈ Finset.Iic n,
    HMul.hMul (α := S)
      ((f : (a : 𝕎 R) → S)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                R) :
            𝕎 R) :
        S)
      (HPow.hPow (α := S) (↑p : S) i)
Tactic: rw [hc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
S : Type u_2
inst_3 : CommRing S
f g : RingHom.{u_1, u_2} (𝕎 R) S
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
      ((g : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
n : ℕ
hn : HPow.hPow (α := S) (↑p : S) n = 0
x c : 𝕎 R
hc :
  x -
      ∑ i ∈ Finset.Iic n,
        HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) =
    HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c
⊢ ∑ i ∈ Finset.Iic n,
      HMul.hMul (α := S)
        ((g : (a : 𝕎 R) → S)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R) :
          S)
        (HPow.hPow (α := S) (↑p : S) i) =
    HAdd.hAdd (α := S) (β := S)
      ((g : (a : 𝕎 R) → S)
          (x -
            ∑ i ∈ Finset.Iic n,
              HMul.hMul (α := 𝕎 R)
                ((teichmuller p : (a : R) → 𝕎 R)
                    ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R)
                        (x.coeff i) :
                      R) :
                  𝕎 R)
                (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S)
      ((g : (a : 𝕎 R) → S)
          (∑ i ∈ Finset.Iic n,
            HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S)
have rw : ∑ i ∈ Finset.Iic n,
    HMul.hMul (α := S)
      ((g : (a : 𝕎 R) → S)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                R) :
            𝕎 R) :
        S)
      (HPow.hPow (α := S) (↑p : S) i) =
  HAdd.hAdd (α := S) (β := S) ((g : (a : 𝕎 R) → S) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c) : S)
    ((g : (a : 𝕎 R) → S)
        (∑ i ∈ Finset.Iic n,
          HMul.hMul (α := 𝕎 R)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R)
            (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
      S)
Tactic: rw [hc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
S : Type u_2
inst_3 : CommRing S
f g : RingHom.{u_1, u_2} (𝕎 R) S
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
      ((g : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
n : ℕ
hn : HPow.hPow (α := S) (↑p : S) n = 0
x c : 𝕎 R
hc :
  x -
      ∑ i ∈ Finset.Iic n,
        HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) =
    HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) x : S) ((g : (a : 𝕎 R) → S) x : S)
have f₁ : (f : (a : 𝕎 R) → S) x =
  HAdd.hAdd (α := S) (β := S)
    ((f : (a : 𝕎 R) → S)
        (x -
          ∑ i ∈ Finset.Iic n,
            HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
      S)
    ((f : (a : 𝕎 R) → S)
        (∑ i ∈ Finset.Iic n,
          HMul.hMul (α := 𝕎 R)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R)
            (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
      S)
Tactic: calc
    f x = f (x - ∑ (i ≤ n), teichmuller p (((_root_.frobeniusEquiv R p).symm ^ i)
        (x.coeff i)) * p ^ i) + f (∑ (i ≤ n), teichmuller p
        (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * p ^ i) := by simp
    _ = ∑ (i ≤ n), f (teichmuller p (((_root_.frobeniusEquiv R p).symm ^ i)
        (x.coeff i))) * p ^ i := by rw [hc]; simp [pow_succ, hn]
    _ = ∑ (i ≤ n), g (teichmuller p
        (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i))) * p ^ i := by simp [h]
    _ = g (x - ∑ (i ≤ n), teichmuller p (((_root_.frobeniusEquiv R p).symm ^ i)
        (x.coeff i)) * p ^ i) + g (∑ (i ≤ n), teichmuller p (((_root_.frobeniusEquiv R p).symm ^ i)
        (x.coeff i)) * p ^ i) := by rw [hc]; simp [pow_succ, hn]
    _ = g x := by simp
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
x : TruncatedWittVector p n R
⊢ (mk p fun (i : Fin n) ↦ coeff i x) = x
have h : ∀ (i : Fin n), coeff i (mk p fun (i : Fin n) ↦ coeff i x) = coeff i x
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
x : TruncatedWittVector p n R
i : Fin n
⊢ coeff i (mk p fun (i : Fin n) ↦ coeff i x) = coeff i x
have h : coeff i x = coeff i x
Tactic: rw [coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ x.out.coeff (↑i : ℕ) = coeff i x
have rw : WittVector.coeff (p := p) { coeff := fun (i : ℕ) ↦ if h : i < n then coeff (⟨i, h⟩ : Fin n) x else 0 } (↑i : ℕ) =
  coeff i x
Tactic: rw [out]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ WittVector.coeff (p := p) { coeff := fun (i : ℕ) ↦ if h : i < n then coeff (⟨i, h⟩ : Fin n) x else 0 } (↑i : ℕ) =
    coeff i x
have dsimp : (if h : (↑i : ℕ) < n then coeff (⟨(↑i : ℕ), h⟩ : Fin n) x else 0) = coeff i x
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ (if h : (↑i : ℕ) < n then coeff (⟨(↑i : ℕ), h⟩ : Fin n) x else 0) = coeff i x
have rw : coeff (⟨(↑i : ℕ), sorry⟩ : Fin n) x = coeff i x
Tactic: rw [dif_pos i.is_lt, Fin.eta]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x y : TruncatedWittVector p n R
h : x.out = y.out
⊢ x = y
have h₁ : ∀ (i : Fin n), coeff i x = coeff i y
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x y : TruncatedWittVector p n R
h : x.out = y.out
i : Fin n
⊢ coeff i x = coeff i y
have h₁ : ∀ (h : ∀ (n_1 : ℕ), x.out.coeff n_1 = y.out.coeff n_1) (i : Fin n), coeff i x = coeff i y
Tactic: rw [WittVector.ext_iff] at h
Cleared hypotheses: h, i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
x : 𝕎 R
i : Fin n
⊢ TruncatedWittVector.coeff i (truncateFun n x) = x.coeff (↑i : ℕ)
have rw : TruncatedWittVector.coeff i (TruncatedWittVector.mk p fun (i : Fin n) ↦ x.coeff (↑i : ℕ)) = x.coeff (↑i : ℕ)
Tactic: rw [truncateFun, TruncatedWittVector.coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
x : 𝕎 R
i : Fin n
rw : TruncatedWittVector.coeff i (TruncatedWittVector.mk p fun (i : Fin n) ↦ x.coeff (↑i : ℕ)) = x.coeff (↑i : ℕ)
⊢ TruncatedWittVector.coeff i (truncateFun n x) = x.coeff (↑i : ℕ)
have rw₁ : x.coeff (↑i : ℕ) = x.coeff (↑i : ℕ)
Tactic: rw [truncateFun, TruncatedWittVector.coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
⊢ (truncateFun n x).out = init n x
have h : ∀ (i : ℕ), (truncateFun n x).out.coeff i = (init n x).coeff i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
i : ℕ
⊢ (truncateFun n x).out.coeff i = (init n x).coeff i
have h : (if h : i < n then TruncatedWittVector.coeff (⟨i, h⟩ : Fin n) (truncateFun n x) else 0) = if i < n then x.coeff i else 0
Tactic: dsimp [TruncatedWittVector.out, init, select, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
i : ℕ
⊢ (if h : i < n then TruncatedWittVector.coeff (⟨i, h⟩ : Fin n) (truncateFun n x) else 0) =
    if i < n then x.coeff i else 0
have pos : ∀ (hi : i < n), TruncatedWittVector.coeff (⟨i, hi⟩ : Fin n) (truncateFun n x) = x.coeff i
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
i : ℕ
pos : ∀ (hi : i < n), TruncatedWittVector.coeff (⟨i, hi⟩ : Fin n) (truncateFun n x) = x.coeff i
⊢ (if h : i < n then TruncatedWittVector.coeff (⟨i, h⟩ : Fin n) (truncateFun n x) else 0) =
    if i < n then x.coeff i else 0
have neg : ∀ (hi : ¬i < n), Eq.{u_1 + 1} (α := R) 0 0
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
⊢ TruncatedWittVector.coeff (⟨i, hi⟩ : Fin n) (truncateFun n x) = x.coeff i
have pos : x.coeff (↑(⟨i, hi⟩ : Fin n) : ℕ) = x.coeff i
Tactic: rw [coeff_truncateFun, Fin.val_mk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
pos : x.coeff (↑(⟨i, hi⟩ : Fin n) : ℕ) = x.coeff i
⊢ TruncatedWittVector.coeff (⟨i, hi⟩ : Fin n) (truncateFun n x) = x.coeff i
have pos₁ : x.coeff i = x.coeff i
Tactic: rw [coeff_truncateFun, Fin.val_mk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
i : Fin n
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) i 0) 0
have change : Eq.{u_1 + 1} (α := R) (coeff (p := p) i (truncateFun n 0)) 0
Tactic: change coeff i (truncateFun _ 0 : TruncatedWittVector p n R) = 0
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
i : Fin n
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) i (truncateFun n 0)) 0
have rw : Eq.{u_1 + 1} (α := R) (WittVector.coeff (p := p) 0 (↑i : ℕ)) 0
Tactic: rw [coeff_truncateFun, WittVector.zero_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
i : Fin n
rw : Eq.{u_1 + 1} (α := R) (WittVector.coeff (p := p) 0 (↑i : ℕ)) 0
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) i (truncateFun n 0)) 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_truncateFun, WittVector.zero_coeff]