-- 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
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
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)
      (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)),
      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 : σ →₀ ℕ)})
      (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 : σ →₀ ℕ)),
      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 : σ →₀ ℕ)})
      (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 : σ →₀ ℕ)),
      HMul.hMul (α := R) (∏ x ∈ range n \ s, (coeff ((k : (a : ℕ) → σ →₀ ℕ) x) : (a : MvPowerSeries σ R) → R) f)
          (∏ x ∈ s, (coeff ((k : (a : ℕ) → σ →₀ ℕ) x) : (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 : σ →₀ ℕ)})
      (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 : σ →₀ ℕ)),
      Eq.{u_3 + 1} (α := R) (∏ x ∈ s, (coeff ((k : (a : ℕ) → σ →₀ ℕ) x) : (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 : σ →₀ ℕ)})
      (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 : σ →₀ ℕ)),
      HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 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 : σ →₀ ℕ)})
      (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 : σ →₀ ℕ)), m ≤ #s
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)
      (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 : σ →₀ ℕ)),
      m + #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤ n
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R) (0 : R)
have rw₃ : ∀ (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)
    (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 : σ →₀ ℕ)),
    m + #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤
      HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ)
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