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
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
hind :
  ∀ (h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)) (n : ℕ),
    Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n_1 n : ℕ
b c : (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
⊢ b = c
have a₁ : (↑b : α) = (↑c : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
hind :
  ∀ (h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)) (n : ℕ),
    Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ insert a S', x s) n) (∑ s ∈ insert a S', (x s).coeff n)
have this : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
Tactic: have : (∀ (n : ℕ), Subsingleton {r | r ∈ S' ∧ (x r).coeff n ≠ 0}) := by
      refine fun n ↦ ⟨fun b c ↦ ?_⟩
      ext
      exact congrArg (fun x ↦ x.1) <|
          (h n).allEq ⟨b.1, S'.subset_insert a b.2.1, b.2.2⟩ ⟨c.1, S'.subset_insert a c.2.1, c.2.2⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
hind :
  ∀ (h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)) (n : ℕ),
    Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
this : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ insert a S', x s) n) (∑ s ∈ insert a S', (x s).coeff n)
have hind₁ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
Tactic: replace hind := hind this
Cleared hypotheses: hind
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
this : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
hind : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ insert a S', x s) n) (∑ s ∈ insert a S', (x s).coeff n)
have insert : (x a + ∑ s ∈ S', x s).coeff n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n
Tactic: simp only [ha, not_false_eq_true, Finset.sum_insert]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
this : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
hind : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
⊢ ∀ (n : ℕ), (x a).coeff n = 0 ∨ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) 0
have simp : ∀ (n : ℕ), (x a).coeff n = 0 ∨ Eq.{u_1 + 1} (α := R) (∑ s ∈ S', (x s).coeff n) 0
Tactic: simp only [hind]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
this : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
hind : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
⊢ ∀ (n : ℕ), (x a).coeff n = 0 ∨ Eq.{u_1 + 1} (α := R) (∑ s ∈ S', (x s).coeff n) 0
have by_contra! : ∀ (m : ℕ) (hma : (x a).coeff m ≠ 0) (hmS' : Ne.{u_1 + 1} (α := R) (∑ s ∈ S', (x s).coeff m) 0), False
Tactic: by_contra! ⟨m, hma, hmS'⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
this : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
hind : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
m : ℕ
hma : (x a).coeff m ≠ 0
hmS' : Ne.{u_1 + 1} (α := R) (∑ s ∈ S', (x s).coeff m) 0
⊢ False
have this₁ : ¬∀ x_1 ∈ S', (x x_1).coeff m = 0
Tactic: have := Finset.sum_eq_zero.mt hmS'
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
this_1 : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
hind : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
m : ℕ
hma : (x a).coeff m ≠ 0
hmS' : Ne.{u_1 + 1} (α := R) (∑ s ∈ S', (x s).coeff m) 0
this : ¬∀ x_1 ∈ S', (x x_1).coeff m = 0
⊢ False
have this₁ : ∃ x_1 ∈ S', (x x_1).coeff m ≠ 0
Tactic: push Not at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
this_1 : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
hind : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
m : ℕ
hma : (x a).coeff m ≠ 0
hmS' : Ne.{u_1 + 1} (α := R) (∑ s ∈ S', (x s).coeff m) 0
this : ∃ x_1 ∈ S', (x x_1).coeff m ≠ 0
⊢ False
have choose : ∀ (b : α) (hb : b ∈ S') (hb' : (x b).coeff m ≠ 0), False
Tactic: choose b hb hb' using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
this : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
hind : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
m : ℕ
hma : (x a).coeff m ≠ 0
hmS' : Ne.{u_1 + 1} (α := R) (∑ s ∈ S', (x s).coeff m) 0
b : α
hb : b ∈ S'
hb' : (x b).coeff m ≠ 0
⊢ False
have this₁ : a = b
Tactic: have : a = b :=
        congrArg (fun x ↦ x.1) <|
          (h m).allEq ⟨a, S'.mem_insert_self a, hma⟩ ⟨b, S'.mem_insert_of_mem hb, hb'⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
this : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
hind : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
⊢ (x a + ∑ s ∈ S', x s).coeff n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n
have this₁ : ∀ (n : ℕ), (x a).coeff n = 0 ∨ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) 0
Tactic: have : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0 := by
      simp only [hind]
      by_contra! ⟨m, hma, hmS'⟩
      have := Finset.sum_eq_zero.mt hmS'
      push Not at this
      choose b hb hb' using this
      have : a = b :=
        congrArg (fun x ↦ x.1) <|
          (h m).allEq ⟨a, S'.mem_insert_self a, hma⟩ ⟨b, S'.mem_insert_of_mem hb, hb'⟩
      exact ha (this ▸ 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
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
this_1 : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
hind : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
this : ∀ (n : ℕ), (x a).coeff n = 0 ∨ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) 0
⊢ (x a + ∑ s ∈ S', x s).coeff n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n
have insert : (x a).coeff n + coeff (p := p) (∑ s ∈ S', x s) n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n
Tactic: rw [coeff_add_of_disjoint n _ _ this, hind 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
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ Insert.insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
this_1 : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
hind : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
this : ∀ (n : ℕ), (x a).coeff n = 0 ∨ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) 0
insert : (x a).coeff n + coeff (p := p) (∑ s ∈ S', x s) n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n
⊢ (x a + ∑ s ∈ S', x s).coeff n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n
have insert₁ : (x a).coeff n + ∑ s ∈ S', (x s).coeff n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n
Tactic: rw [coeff_add_of_disjoint n _ _ this, hind 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
α : Type u_2
S : Finset α
x : α → 𝕎 R
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S, x s) n) (∑ s ∈ S, (x s).coeff n)
have empty : ∀ (h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | Membership.mem (γ := Finset α) ∅ r ∧ (x r).coeff n ≠ 0} : Type u_2))
  (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ ∅, x s) n) (∑ s ∈ ∅, (x s).coeff n)
Tactic: induction S using Finset.induction generalizing n with
  | empty =>
    simp
  | insert a S' ha hind =>
    have : (∀ (n : ℕ), Subsingleton {r | r ∈ S' ∧ (x r).coeff n ≠ 0}) := by
      refine fun n ↦ ⟨fun b c ↦ ?_⟩
      ext
      exact congrArg (fun x ↦ x.1) <|
          (h n).allEq ⟨b.1, S'.subset_insert a b.2.1, b.2.2⟩ ⟨c.1, S'.subset_insert a c.2.1, c.2.2⟩
    replace hind := hind this
    simp only [ha, not_false_eq_true, Finset.sum_insert]
    have : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0 := by
      simp only [hind]
      by_contra! ⟨m, hma, hmS'⟩
      have := Finset.sum_eq_zero.mt hmS'
      push Not at this
      choose b hb hb' using this
      have : a = b :=
        congrArg (fun x ↦ x.1) <|
          (h m).allEq ⟨a, S'.mem_insert_self a, hma⟩ ⟨b, S'.mem_insert_of_mem hb, hb'⟩
      exact ha (this ▸ hb)
    rw [coeff_add_of_disjoint n _ _ this, hind n]
Cleared hypotheses: S, h, 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
α : Type u_2
S : Finset α
x : α → 𝕎 R
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
empty :
  ∀
    (h :
      ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | Membership.mem (γ := Finset α) ∅ r ∧ (x r).coeff n ≠ 0} : Type u_2))
    (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ ∅, x s) n) (∑ s ∈ ∅, (x s).coeff n)
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S, x s) n) (∑ s ∈ S, (x s).coeff n)
have insert : ∀ (a : α) (S' : Finset α) (ha : a ∉ S')
  (hind :
    ∀ (h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)) (n : ℕ),
      Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n))
  (h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)) (n : ℕ),
  Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ insert a S', x s) n) (∑ s ∈ insert a S', (x s).coeff n)
Tactic: induction S using Finset.induction generalizing n with
  | empty =>
    simp
  | insert a S' ha hind =>
    have : (∀ (n : ℕ), Subsingleton {r | r ∈ S' ∧ (x r).coeff n ≠ 0}) := by
      refine fun n ↦ ⟨fun b c ↦ ?_⟩
      ext
      exact congrArg (fun x ↦ x.1) <|
          (h n).allEq ⟨b.1, S'.subset_insert a b.2.1, b.2.2⟩ ⟨c.1, S'.subset_insert a c.2.1, c.2.2⟩
    replace hind := hind this
    simp only [ha, not_false_eq_true, Finset.sum_insert]
    have : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0 := by
      simp only [hind]
      by_contra! ⟨m, hma, hmS'⟩
      have := Finset.sum_eq_zero.mt hmS'
      push Not at this
      choose b hb hb' using this
      have : a = b :=
        congrArg (fun x ↦ x.1) <|
          (h m).allEq ⟨a, S'.mem_insert_self a, hma⟩ ⟨b, S'.mem_insert_of_mem hb, hb'⟩
      exact ha (this ▸ hb)
    rw [coeff_add_of_disjoint n _ _ this, hind n]
Cleared hypotheses: S, h, 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
α : Type u_2
S : Finset α
x : α → 𝕎 R
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S, x s) n) (∑ s ∈ S, (x s).coeff n)
have empty : ∀ (h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | Membership.mem (γ := Finset α) ∅ r ∧ (x r).coeff n ≠ 0} : Type u_2))
  (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ ∅, x s) n) (∑ s ∈ ∅, (x s).coeff n)
Tactic: classical
  induction S using Finset.induction generalizing n with
  | empty =>
    simp
  | insert a S' ha hind =>
    have : (∀ (n : ℕ), Subsingleton {r | r ∈ S' ∧ (x r).coeff n ≠ 0}) := by
      refine fun n ↦ ⟨fun b c ↦ ?_⟩
      ext
      exact congrArg (fun x ↦ x.1) <|
          (h n).allEq ⟨b.1, S'.subset_insert a b.2.1, b.2.2⟩ ⟨c.1, S'.subset_insert a c.2.1, c.2.2⟩
    replace hind := hind this
    simp only [ha, not_false_eq_true, Finset.sum_insert]
    have : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0 := by
      simp only [hind]
      by_contra! ⟨m, hma, hmS'⟩
      have := Finset.sum_eq_zero.mt hmS'
      push Not at this
      choose b hb hb' using this
      have : a = b :=
        congrArg (fun x ↦ x.1) <|
          (h m).allEq ⟨a, S'.mem_insert_self a, hma⟩ ⟨b, S'.mem_insert_of_mem hb, hb'⟩
      exact ha (this ▸ hb)
    rw [coeff_add_of_disjoint n _ _ this, hind n]
Cleared hypotheses: S, h, 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
α : Type u_2
S : Finset α
x : α → 𝕎 R
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
empty :
  ∀
    (h :
      ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | Membership.mem (γ := Finset α) ∅ r ∧ (x r).coeff n ≠ 0} : Type u_2))
    (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ ∅, x s) n) (∑ s ∈ ∅, (x s).coeff n)
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S, x s) n) (∑ s ∈ S, (x s).coeff n)
have insert : ∀ (a : α) (S' : Finset α) (ha : a ∉ S')
  (hind :
    ∀ (h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)) (n : ℕ),
      Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n))
  (h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)) (n : ℕ),
  Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ insert a S', x s) n) (∑ s ∈ insert a S', (x s).coeff n)
Tactic: classical
  induction S using Finset.induction generalizing n with
  | empty =>
    simp
  | insert a S' ha hind =>
    have : (∀ (n : ℕ), Subsingleton {r | r ∈ S' ∧ (x r).coeff n ≠ 0}) := by
      refine fun n ↦ ⟨fun b c ↦ ?_⟩
      ext
      exact congrArg (fun x ↦ x.1) <|
          (h n).allEq ⟨b.1, S'.subset_insert a b.2.1, b.2.2⟩ ⟨c.1, S'.subset_insert a c.2.1, c.2.2⟩
    replace hind := hind this
    simp only [ha, not_false_eq_true, Finset.sum_insert]
    have : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0 := by
      simp only [hind]
      by_contra! ⟨m, hma, hmS'⟩
      have := Finset.sum_eq_zero.mt hmS'
      push Not at this
      choose b hb hb' using this
      have : a = b :=
        congrArg (fun x ↦ x.1) <|
          (h m).allEq ⟨a, S'.mem_insert_self a, hma⟩ ⟨b, S'.mem_insert_of_mem hb, hb'⟩
      exact ha (this ▸ hb)
    rw [coeff_add_of_disjoint n _ _ this, hind n]
Cleared hypotheses: S, h, 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
x : R
m n : ℕ
h_1 : m ≠ n
h : n < m
⊢ (HMul.hMul (α := 𝕎 R) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n)).coeff m = 0
have inr : p ^ n ≠ 0
Tactic: rw [← Nat.sub_add_cancel h.le, WittVector.mul_pow_charP_coeff_succ (teichmuller p x),
      WittVector.teichmuller_coeff_pos p x (m - n) (Nat.zero_lt_sub_of_lt h), zero_pow]
-- 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
x : R
m n : ℕ
h : m ≠ n
⊢ (HMul.hMul (α := 𝕎 R) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n)).coeff m = 0
have x₁ : m < n ∨ n < m
Tactic: cases Nat.lt_or_lt_of_ne h with
  | inl h =>
    exact WittVector.mul_pow_charP_coeff_zero (teichmuller p x) h
  | inr h =>
    rw [← Nat.sub_add_cancel h.le, WittVector.mul_pow_charP_coeff_succ (teichmuller p x),
      WittVector.teichmuller_coeff_pos p x (m - n) (Nat.zero_lt_sub_of_lt h), zero_pow]
    simp [Nat.Prime.ne_zero Fact.out]
-- 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 : ℕ
⊢ HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) ∣
    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)
have rw : ∀ i < n + 1,
  x.coeff i =
    coeff (p := p)
      (∑ 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))
      i
Tactic: rw [← Ideal.mem_span_singleton, mem_span_p_pow_iff_le_coeff_eq_zero,
      ← le_coeff_eq_iff_le_sub_coeff_eq_zero]
-- 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
⊢ x.coeff i =
    coeff (p := p)
      (∑ 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))
      i
have rw : x.coeff i =
  ∑ s ∈ Finset.Iic n,
    (HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) s : (a : R) → R) (x.coeff s) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) s)).coeff
      i
Tactic: rw [WittVector.sum_coeff_eq_coeff_sum]
-- 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
rw :
  x.coeff i =
    ∑ s ∈ Finset.Iic n,
      (HMul.hMul (α := 𝕎 R)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) s : (a : R) → R) (x.coeff s) :
                  R) :
              𝕎 R)
            (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) s)).coeff
        i
⊢ x.coeff i =
    coeff (p := p)
      (∑ 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))
      i
have h : ∀ (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: rw [WittVector.sum_coeff_eq_coeff_sum]
-- 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
⊢ x.coeff i =
    ∑ s ∈ Finset.Iic n,
      (HMul.hMul (α := 𝕎 R)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) s : (a : R) → R) (x.coeff s) :
                  R) :
              𝕎 R)
            (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) s)).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 +
    ∑ 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_eq_add_sum_diff_singleton_of_mem (Finset.mem_Iic.mpr (Nat.lt_succ_iff.mp hi))]