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
α : 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 : ℕ
refine : ∀ (n : ℕ) (b c : (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)), b = c
⊢ ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)

Tactic:
refine fun n ↦ ⟨fun b c ↦ ?_⟩
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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)
a₁ : (↑b : α) = (↑c : α)
⊢ b = c

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

Tactic:
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⟩

Premises used: congrArg, Subtype.mk, Subsingleton.allEq, And.right, And.left, And.intro, Finset.subset_insert, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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 : α)

Tactic:
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⟩

Premises used: congrArg, Subtype.mk, Subsingleton.allEq, And.right, And.left, And.intro, Finset.subset_insert, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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 : ℕ
⊢ ∀ (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⟩
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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)
⊢ ∀ (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
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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 : ∀ (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)
insert : (x a + ∑ s ∈ S', x s).coeff n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ Insert.insert a S', x s) n) (∑ s ∈ Insert.insert a S', (x s).coeff n)

Tactic:
simp only [ha, not_false_eq_true, Finset.sum_insert]

Premises used: Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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)
simp : ∀ (n : ℕ), (x a).coeff n = 0 ∨ Eq.{u_1 + 1} (α := R) (∑ s ∈ S', (x s).coeff n) 0
⊢ ∀ (n : ℕ), (x a).coeff n = 0 ∨ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) 0

Tactic:
simp only [hind]
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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)
by_contra! : ∀ (m : ℕ) (hma : (x a).coeff m ≠ 0) (hmS' : Ne.{u_1 + 1} (α := R) (∑ s ∈ S', (x s).coeff m) 0), False
⊢ ∀ (n : ℕ), (x a).coeff n = 0 ∨ Eq.{u_1 + 1} (α := R) (∑ s ∈ S', (x s).coeff n) 0

Tactic:
by_contra! ⟨m, hma, hmS'⟩
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
⊢ ¬∀ x_1 ∈ S', (x x_1).coeff m = 0

Tactic:
have := Finset.sum_eq_zero.mt hmS'
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
⊢ ∃ x_1 ∈ S', (x x_1).coeff m ≠ 0

Tactic:
push Not at this

Premises used: Not
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
choose : ∀ (b : α) (hb : b ∈ S') (hb' : (x b).coeff m ≠ 0), False
⊢ False

Tactic:
choose b hb hb' using this
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
⊢ 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'⟩
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
b : α
hb : b ∈ S'
hb' : (x b).coeff m ≠ 0
this : a = b
⊢ False

Tactic:
ha (this ▸ hb)

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
b : α
hb : b ∈ S'
hb' : (x b).coeff m ≠ 0
this : a = b
⊢ False

Tactic:
exact ha (this ▸ hb)

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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

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)
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
insert₁ insert₂ : (x a).coeff n + ∑ s ∈ S', (x s).coeff 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

Tactic:
rw [coeff_add_of_disjoint n _ _ this, hind n]

Premises used: WittVector.coeff_add_of_disjoint
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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)
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.insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)) (n : ℕ),
    Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ Insert.insert a S', x s) n) (∑ s ∈ Insert.insert a S', (x s).coeff n)
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S, x s) n) (∑ s ∈ 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]

Premises used: Insert.insert, Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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)
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.insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)) (n : ℕ),
    Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ Insert.insert a S', x s) n) (∑ s ∈ Insert.insert a S', (x s).coeff n)
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S, x s) n) (∑ s ∈ 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]

Premises used: Insert.insert, Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
n : ℕ
x : R
⊢ (HMul.hMul (α := 𝕎 R) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n)).coeff n =
    x ^ p ^ n

Tactic:
simpa using WittVector.mul_pow_charP_coeff_succ (teichmuller p x) (m := 0)

Premises used: DFunLike.coe, WittVector.mul_pow_charP_coeff_succ, WittVector.teichmuller
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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 : m < n
⊢ (HMul.hMul (α := 𝕎 R) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n)).coeff m = 0

Tactic:
WittVector.mul_pow_charP_coeff_zero (teichmuller p x) h

Premises used: WittVector.mul_pow_charP_coeff_zero, DFunLike.coe, WittVector.teichmuller
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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 : m < n
⊢ (HMul.hMul (α := 𝕎 R) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n)).coeff m = 0

Tactic:
exact WittVector.mul_pow_charP_coeff_zero (teichmuller p x) h

Premises used: WittVector.mul_pow_charP_coeff_zero, DFunLike.coe, WittVector.teichmuller
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
inr : p ^ n ≠ 0
⊢ (HMul.hMul (α := 𝕎 R) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n)).coeff m = 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]

Premises used: Nat.zero_lt_sub_of_lt, HSub.hSub, LT.lt.le, Nat.sub_add_cancel, WittVector.teichmuller_coeff_pos, DFunLike.coe, WittVector.mul_pow_charP_coeff_succ, zero_pow, WittVector.teichmuller
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
⊢ p ^ n ≠ 0

Tactic:
simp [Nat.Prime.ne_zero Fact.out]

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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
⊢ 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]

Premises used: Nat.lt_or_lt_of_ne, WittVector.mul_pow_charP_coeff_zero, Nat.Prime.ne_zero, DFunLike.coe, WittVector.mul_pow_charP_coeff_succ, zero_pow, WittVector.teichmuller, Fact.out
-- 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 : ℕ
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
⊢ 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)

Tactic:
rw [← Ideal.mem_span_singleton, mem_span_p_pow_iff_le_coeff_eq_zero,
      ← le_coeff_eq_iff_le_sub_coeff_eq_zero]

Premises used: WittVector.mem_span_p_pow_iff_le_coeff_eq_zero, Ideal.mem_span_singleton, WittVector.le_coeff_eq_iff_le_sub_coeff_eq_zero
-- 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
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
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)
⊢ 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 [WittVector.sum_coeff_eq_coeff_sum]

Premises used: WittVector.sum_coeff_eq_coeff_sum
-- 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
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
⊢ 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 [Finset.sum_eq_add_sum_diff_singleton_of_mem (Finset.mem_Iic.mpr (Nat.lt_succ_iff.mp hi))]

Premises used: Iff.mpr, Finset.mem_Iic, Nat.lt_succ_iff, Iff.mp, Finset.sum_eq_add_sum_diff_singleton_of_mem