awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
h : #(range n \ s) = HSMul.hSMul (β := ℕ) (#(range n \ s)) 1
h₁ :
  Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x) : ℕ)
    (∑ x ∈ range n \ s, (degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) : ℕ)
⊢ #(range n \ s) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x)
have convert! : ∀ x ∈ range n \ s,
  LE.le (α := ℕ) 1 ((fun (x : ℕ) ↦ ((degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) : ℕ)) x)
Tactic: convert! Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
⊢ ∀ x ∈ range n \ s,
    LE.le (α := ℕ) 1 ((fun (x : ℕ) ↦ ((degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) : ℕ)) x)
have simp : ∀ x < n,
  (x < n → ¬Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) (0 : σ →₀ ℕ)) →
    LE.le (α := ℕ) (1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) : ℕ)
Tactic: simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
i : ℕ
hi : i < n
hi' : i < n → ¬Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
⊢ LE.le (α := ℕ) (1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) : ℕ)
have rw : ¬Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
Tactic: rw [← not_lt, Nat.lt_one_iff, degree_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R) (0 : R)
have rw : Eq.{u_3 + 1} (α := R)
  (∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
  0
Tactic: classical
  rw [coeff_pow]
  apply sum_eq_zero
  intro k hk
  rw [mem_finsuppAntidiag] at hk
  set s := {i ∈ range n | k i = 0} with hs_def
  have hs : s ⊆ range n := filter_subset _ _
  have hs' (i : ℕ) (hi : i ∈ s) : coeff (k i) f = constantCoeff f := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2, coeff_zero_eq_constantCoeff]
  have hs'' (i : ℕ) (hi : i ∈ s) : k i = 0 := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2]
  rw [← prod_sdiff (s₁ := s) (filter_subset _ _)]
  apply mul_eq_zero_of_right
  rw [prod_congr rfl hs', prod_const]
  suffices m ≤ #s by
    obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
    rw [hm', pow_add, hf, zero_mul]
  rw [← Nat.add_le_add_iff_right, add_comm #s,
    Finset.card_sdiff_add_card_eq_card (filter_subset _ _), card_range]
  apply le_trans _ hn
  simp only [add_comm m, Nat.add_le_add_iff_right, ← hk.1,
    ← sum_sdiff (hs), sum_eq_zero (s := s) hs'', add_zero]
  rw [← hs_def]
  convert! Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _
  · simp only [smul_eq_mul, mul_one]
  · simp only [degree_eq_weight_one, map_sum]
  · simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
    intro i hi hi'
    rw [← not_lt, Nat.lt_one_iff, degree_eq_zero_iff]
    exact hi' hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
rw rw₁ rw₂ :
  Eq.{u_3 + 1} (α := R)
    (∑ l ∈ (range n).finsuppAntidiag d,
      ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
    0
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R) (0 : R)
have h : ∀ (x : ℕ →₀ σ →₀ ℕ),
  Membership.mem (γ := Finset (ℕ →₀ σ →₀ ℕ)) ((range n).finsuppAntidiag d) x →
    Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((x : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
Tactic: classical
  rw [coeff_pow]
  apply sum_eq_zero
  intro k hk
  rw [mem_finsuppAntidiag] at hk
  set s := {i ∈ range n | k i = 0} with hs_def
  have hs : s ⊆ range n := filter_subset _ _
  have hs' (i : ℕ) (hi : i ∈ s) : coeff (k i) f = constantCoeff f := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2, coeff_zero_eq_constantCoeff]
  have hs'' (i : ℕ) (hi : i ∈ s) : k i = 0 := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2]
  rw [← prod_sdiff (s₁ := s) (filter_subset _ _)]
  apply mul_eq_zero_of_right
  rw [prod_congr rfl hs', prod_const]
  suffices m ≤ #s by
    obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
    rw [hm', pow_add, hf, zero_mul]
  rw [← Nat.add_le_add_iff_right, add_comm #s,
    Finset.card_sdiff_add_card_eq_card (filter_subset _ _), card_range]
  apply le_trans _ hn
  simp only [add_comm m, Nat.add_le_add_iff_right, ← hk.1,
    ← sum_sdiff (hs), sum_eq_zero (s := s) hs'', add_zero]
  rw [← hs_def]
  convert! Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _
  · simp only [smul_eq_mul, mul_one]
  · simp only [degree_eq_weight_one, map_sum]
  · simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
    intro i hi hi'
    rw [← not_lt, Nat.lt_one_iff, degree_eq_zero_iff]
    exact hi' hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
rw rw₁ rw₂ :
  Eq.{u_3 + 1} (α := R)
    (∑ l ∈ (range n).finsuppAntidiag d,
      ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
    0
h h₁ :
  ∀ (k : ℕ →₀ σ →₀ ℕ) (hk : Membership.mem (γ := Finset (ℕ →₀ σ →₀ ℕ)) ((range n).finsuppAntidiag d) k),
    Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R) (0 : R)
have h₂ : ∀ (k : ℕ →₀ σ →₀ ℕ) (hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n),
  Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
Tactic: classical
  rw [coeff_pow]
  apply sum_eq_zero
  intro k hk
  rw [mem_finsuppAntidiag] at hk
  set s := {i ∈ range n | k i = 0} with hs_def
  have hs : s ⊆ range n := filter_subset _ _
  have hs' (i : ℕ) (hi : i ∈ s) : coeff (k i) f = constantCoeff f := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2, coeff_zero_eq_constantCoeff]
  have hs'' (i : ℕ) (hi : i ∈ s) : k i = 0 := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2]
  rw [← prod_sdiff (s₁ := s) (filter_subset _ _)]
  apply mul_eq_zero_of_right
  rw [prod_congr rfl hs', prod_const]
  suffices m ≤ #s by
    obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
    rw [hm', pow_add, hf, zero_mul]
  rw [← Nat.add_le_add_iff_right, add_comm #s,
    Finset.card_sdiff_add_card_eq_card (filter_subset _ _), card_range]
  apply le_trans _ hn
  simp only [add_comm m, Nat.add_le_add_iff_right, ← hk.1,
    ← sum_sdiff (hs), sum_eq_zero (s := s) hs'', add_zero]
  rw [← hs_def]
  convert! Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _
  · simp only [smul_eq_mul, mul_one]
  · simp only [degree_eq_weight_one, map_sum]
  · simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
    intro i hi hi'
    rw [← not_lt, Nat.lt_one_iff, degree_eq_zero_iff]
    exact hi' hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
rw rw₁ rw₂ :
  Eq.{u_3 + 1} (α := R)
    (∑ l ∈ (range n).finsuppAntidiag d,
      ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
    0
h h₁ :
  ∀ (k : ℕ →₀ σ →₀ ℕ) (hk : Membership.mem (γ := Finset (ℕ →₀ σ →₀ ℕ)) ((range n).finsuppAntidiag d) k),
    Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
h₂ :
  ∀ (k : ℕ →₀ σ →₀ ℕ) (hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n),
    Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R) (0 : R)
have h₃ : ∀ (k : ℕ →₀ σ →₀ ℕ) (hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n),
  let s := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)};
  ∀ (hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}),
    Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
Tactic: classical
  rw [coeff_pow]
  apply sum_eq_zero
  intro k hk
  rw [mem_finsuppAntidiag] at hk
  set s := {i ∈ range n | k i = 0} with hs_def
  have hs : s ⊆ range n := filter_subset _ _
  have hs' (i : ℕ) (hi : i ∈ s) : coeff (k i) f = constantCoeff f := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2, coeff_zero_eq_constantCoeff]
  have hs'' (i : ℕ) (hi : i ∈ s) : k i = 0 := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2]
  rw [← prod_sdiff (s₁ := s) (filter_subset _ _)]
  apply mul_eq_zero_of_right
  rw [prod_congr rfl hs', prod_const]
  suffices m ≤ #s by
    obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
    rw [hm', pow_add, hf, zero_mul]
  rw [← Nat.add_le_add_iff_right, add_comm #s,
    Finset.card_sdiff_add_card_eq_card (filter_subset _ _), card_range]
  apply le_trans _ hn
  simp only [add_comm m, Nat.add_le_add_iff_right, ← hk.1,
    ← sum_sdiff (hs), sum_eq_zero (s := s) hs'', add_zero]
  rw [← hs_def]
  convert! Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _
  · simp only [smul_eq_mul, mul_one]
  · simp only [degree_eq_weight_one, map_sum]
  · simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
    intro i hi hi'
    rw [← not_lt, Nat.lt_one_iff, degree_eq_zero_iff]
    exact hi' hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
rw rw₁ rw₂ :
  Eq.{u_3 + 1} (α := R)
    (∑ l ∈ (range n).finsuppAntidiag d,
      ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
    0
h h₁ :
  ∀ (k : ℕ →₀ σ →₀ ℕ) (hk : Membership.mem (γ := Finset (ℕ →₀ σ →₀ ℕ)) ((range n).finsuppAntidiag d) k),
    Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
h₂ :
  ∀ (k : ℕ →₀ σ →₀ ℕ) (hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n),
    Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
h₃ :
  ∀ (k : ℕ →₀ σ →₀ ℕ) (hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n),
    let s := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)};
    ∀ (hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}),
      Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R) (0 : R)
have h₄ : ∀ (k : ℕ →₀ σ →₀ ℕ) (hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n),
  let s := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)};
  ∀ (hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) (hs : s ⊆ range n),
    Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
Tactic: classical
  rw [coeff_pow]
  apply sum_eq_zero
  intro k hk
  rw [mem_finsuppAntidiag] at hk
  set s := {i ∈ range n | k i = 0} with hs_def
  have hs : s ⊆ range n := filter_subset _ _
  have hs' (i : ℕ) (hi : i ∈ s) : coeff (k i) f = constantCoeff f := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2, coeff_zero_eq_constantCoeff]
  have hs'' (i : ℕ) (hi : i ∈ s) : k i = 0 := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2]
  rw [← prod_sdiff (s₁ := s) (filter_subset _ _)]
  apply mul_eq_zero_of_right
  rw [prod_congr rfl hs', prod_const]
  suffices m ≤ #s by
    obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
    rw [hm', pow_add, hf, zero_mul]
  rw [← Nat.add_le_add_iff_right, add_comm #s,
    Finset.card_sdiff_add_card_eq_card (filter_subset _ _), card_range]
  apply le_trans _ hn
  simp only [add_comm m, Nat.add_le_add_iff_right, ← hk.1,
    ← sum_sdiff (hs), sum_eq_zero (s := s) hs'', add_zero]
  rw [← hs_def]
  convert! Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _
  · simp only [smul_eq_mul, mul_one]
  · simp only [degree_eq_weight_one, map_sum]
  · simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
    intro i hi hi'
    rw [← not_lt, Nat.lt_one_iff, degree_eq_zero_iff]
    exact hi' hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
a : R
φ : MvPowerSeries σ A
⊢ HMul.hMul (α := MvPowerSeries σ A)
      ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ A) a : MvPowerSeries σ A) φ =
    HMul.hMul (β := MvPowerSeries σ A) φ
      ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ A) a : MvPowerSeries σ A)
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_3 + 1} (α := A)
    ((coeff n : (a : MvPowerSeries σ A) → A)
        (HMul.hMul (α := MvPowerSeries σ A)
          ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ A) a : MvPowerSeries σ A) φ) :
      A)
    ((coeff n : (a : MvPowerSeries σ A) → A)
        (HMul.hMul (β := MvPowerSeries σ A) φ
          ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ A) a : MvPowerSeries σ A)) :
      A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ_1 : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
a : R
σ : MvPowerSeries σ_1 A
⊢ a • σ =
    HMul.hMul (α := MvPowerSeries σ_1 A)
      ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ_1 A) a : MvPowerSeries σ_1 A) σ
have h : ∀ (n : σ_1 →₀ ℕ),
  Eq.{u_3 + 1} (α := A) ((coeff n : (a : MvPowerSeries σ_1 A) → A) (a • σ) : A)
    ((coeff n : (a : MvPowerSeries σ_1 A) → A)
        (HMul.hMul (α := MvPowerSeries σ_1 A)
          ((RingHom.comp (map (algebraMap R A)) C : (a : R) → MvPowerSeries σ_1 A) a : MvPowerSeries σ_1 A) σ) :
      A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
⊢ Ne (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
have rw : ∃ (x : MvPowerSeries σ R),
  ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
Tactic: rw [Ne, SetLike.ext_iff, not_forall]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
⊢ ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
have inhabit : ∀ (inhabited_h : Inhabited σ),
  ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
Tactic: inhabit σ
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
inhabited_h : Inhabited σ
⊢ ∃ (x : MvPowerSeries σ R),
    ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
        Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x)
have refine : ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ (X default) ↔
    Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ (X default))
Tactic: refine ⟨X default, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
inhabited_h : Inhabited σ
⊢ ¬(Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ (X default) ↔
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ (X default))
have simp : ∀ (x : R),
  ¬Eq (α := MvPowerSeries σ R) ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R)
      (X default : MvPowerSeries σ R)
Tactic: simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
inhabited_h : Inhabited σ
x : R
⊢ ¬Eq (α := MvPowerSeries σ R) ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R)
      (X default : MvPowerSeries σ R)
have rw : ∃ (x_1 : σ →₀ ℕ),
  ¬Eq.{u_2 + 1} (α := R)
      ((coeff x_1 : (a : MvPowerSeries σ R) → R)
          ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
      ((coeff x_1 : (a : MvPowerSeries σ R) → R) (X default) : R)
Tactic: rw [MvPowerSeries.ext_iff, not_forall]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
inhabited_h : Inhabited σ
x : R
⊢ ∃ (x_1 : σ →₀ ℕ),
    ¬Eq.{u_2 + 1} (α := R)
        ((coeff x_1 : (a : MvPowerSeries σ R) → R)
            ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
          R)
        ((coeff x_1 : (a : MvPowerSeries σ R) → R) (X default) : R)
have refine : ¬Eq.{u_2 + 1} (α := R)
    ((coeff (single default 1) : (a : MvPowerSeries σ R) → R)
        ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
    ((coeff (single default 1) : (a : MvPowerSeries σ R) → R) (X default) : R)
Tactic: refine ⟨Finsupp.single default 1, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
⊢ Ne (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
have rw : ¬Eq (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
Tactic: classical
      rw [Ne, SetLike.ext_iff, not_forall]
      inhabit σ
      refine ⟨X default, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
      intro x
      rw [MvPowerSeries.ext_iff, not_forall]
      refine ⟨Finsupp.single default 1, ?_⟩
      simp [algebraMap_apply, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nonempty σ
inst_6 : Nontrivial R
rw : ¬Eq (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
⊢ Ne (α := Subalgebra R (MvPowerSeries σ R)) ⊥ ⊤
have rw₁ : ¬∀ (x : MvPowerSeries σ R),
    Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊥ x ↔
      Membership.mem (γ := Subalgebra R (MvPowerSeries σ R)) ⊤ x
Tactic: classical
      rw [Ne, SetLike.ext_iff, not_forall]
      inhabit σ
      refine ⟨X default, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
      intro x
      rw [MvPowerSeries.ext_iff, not_forall]
      refine ⟨Finsupp.single default 1, ?_⟩
      simp [algebraMap_apply, coeff_C]