awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
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
⊢ 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

Tactic:
rw [Finset.sum_congr rfl (g := g)]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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 +
      (Finset.Iic n \ {i}).sum g

Tactic:
simp [g]
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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}
⊢ b ≤ n ∧ ¬b = i

Tactic:
simp only [Finset.mem_sdiff, Finset.mem_Iic, Finset.mem_singleton] at hb

Premises used: Finset.mem_singleton, Finset.mem_Iic, Finset.mem_sdiff
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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 ≤ n ∧ ¬b = 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

Tactic:
teichmuller_mul_pow_coeff_of_ne _ (Ne.intro hb.2).symm

Premises used: WittVector.teichmuller_mul_pow_coeff_of_ne, Ne.symm, And.right, Ne.intro
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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 ≤ n ∧ ¬b = 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

Tactic:
exact teichmuller_mul_pow_coeff_of_ne _ (Ne.intro hb.2).symm

Premises used: WittVector.teichmuller_mul_pow_coeff_of_ne, Ne.symm, And.right, Ne.intro
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
⊢ ∀ (n_1 : ℕ),
    Subsingleton
      (↑{r : ℕ |
            r ∈ Finset.Iic n ∧
              (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_1 ≠
                0} :
        Type)

Tactic:
fun n ↦ ⟨fun ⟨a, _, ha⟩ ⟨b, _, hb⟩ ↦ ?_⟩

Premises used: Subtype.mk, Subsingleton.intro, And.intro, Eq, _private.0.WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff.match_3
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
h : a = b
⊢ (↑(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 ⋯) :
      ℕ)

Tactic:
dsimp only [ne_eq, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, ne_eq
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
h : n = b
⊢ a = b

Tactic:
rw [← Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) ha]

Premises used: WittVector.teichmuller_mul_pow_coeff_of_ne, Not.imp_symm
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
⊢ n = b

Tactic:
Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) hb

Premises used: WittVector.teichmuller_mul_pow_coeff_of_ne, Not.imp_symm
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
⊢ n = b

Tactic:
exact Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) hb

Premises used: WittVector.teichmuller_mul_pow_coeff_of_ne, Not.imp_symm
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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)
obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := S) (↑p : S) n = 0), f = g
⊢ f = g

Tactic:
obtain ⟨n, hn⟩ := hp
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
a : ∀ (x : 𝕎 R), Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) x : S) ((g : (a : 𝕎 R) → S) x : S)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
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)
⊢ 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)

Premises used: WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
⊢ (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:
simp
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
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)
⊢ 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)

Tactic:
rw [hc]
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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) (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:
simp [pow_succ, hn]

Premises used: pow_succ
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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)
    (∑ 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))
    (∑ 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))

Tactic:
simp [h]