-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
simp :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ a.support.piAntidiag n,
      if s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support x) : R)
          (∏ x_1 ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x_1 : R) (x x_1))
      else 0)
    0
simp₁ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n),
    (if s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support x) : R)
          (∏ x_1 ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x_1 : R) (x x_1))
      else 0) =
      0
hnc : ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n), ¬s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i
hnc₁ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n)
    (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n), False
hnc₂ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n)
    (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n),
    (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
hnc₃ :
  ∀ (x : σ → ℕ) (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n)
    (hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support),
    (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
hnc₄ :
  ∀ (x : σ → ℕ) (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n)
    (hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support),
    ∑ x_1 ∈ a.support, (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1 = a.support.sum x
hnc₅ :
  ∀ (x : σ → ℕ) (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n)
    (hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support),
    (fun (x_1 : σ) ↦ (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1) = x
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    0
have hnc₆ : ∀ (x : σ → ℕ) (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n)
  (hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support) (i : σ),
  (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i
Tactic: classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  apply Finset.sum_eq_zero (fun x hx ↦ ?_)
  rw [if_neg]
  rintro ⟨rfl⟩
  apply hs
  simp only [Finset.mem_piAntidiag] at hx
  rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
  congr
  ext i
  by_cases hi : i ∈ a.support
  · simp [Finsupp.indicator_of_mem hi]
  · grind [Finsupp.indicator_of_notMem hi]
Cleared hypotheses: s, hs