-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d
empty :
  ∀
    (hd :
      ∀ (b : ι),
        Membership.mem (γ := Finset ι) ∅ b →
          (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ ∅, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ ∅, g b) (∑ b₁ ∈ ∅, ∑ b₂ ∈ ∅, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
insert :
  ∀ (b : ι) (B : Finset ι) (hb : b ∉ B)
    (h :
      ∀ (hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
        (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d),
        ∃ (c : ι → ι → R),
          Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)))
    (hd :
      ∀ b_1 ∈ Insert.insert b B,
        (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) = d ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ Insert.insert b B, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ Insert.insert b B, g b)
        (∑ b₁ ∈ Insert.insert b B, ∑ b₂ ∈ Insert.insert b B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
⊢ ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))

Tactic:
classical
  induction B using Finset.induction_on with
  | empty => simp
  | insert b B hb h =>
    by_cases hb0 : g b = 0
    · simp_all
    simp? [Finset.sum_insert hb, hb0] at hfd hd says
      simp only [Finset.sum_insert hb, Finset.mem_insert, forall_eq_or_imp, hb0, or_false]
        at hfd hd
    obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd
    use fun b₁ b₂ ↦ if b₂ = b then ↑isunit_gb.unit⁻¹ else 0
    simp? [Finset.sum_insert hb, hb] says
      simp only [Finset.sum_insert hb, ite_smul, zero_smul, ↓reduceIte, Finset.sum_ite_eq', hb,
        add_zero, sPolynomial_self, smul_zero, zero_add]
    simp only [m.toSyn.injective.eq_iff] at *
    trans ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b)
    · suffices (-(∑ i ∈ B, m.leadingCoeff (g i))) = m.leadingCoeff (g b) by
        rw [add_comm, Finset.sum_sub_distrib, sub_eq_add_neg, ← Finset.sum_smul, ← Finset.sum_mul,
          ← neg_smul, ← neg_mul, this, isunit_gb.mul_val_inv, one_smul]
      rw [← add_eq_zero_iff_neg_eq']
      trans (g b).coeff (m.degree <| g b) + ∑ i ∈ B, (g i).coeff (m.degree <| g b)
      · unfold leadingCoeff
        congr 1
        apply Finset.sum_congr rfl
        intro b' hb'
        rcases hd b' hb' with h | h <;> simp [h]
      · rw [← coeff_sum, ← coeff_add, ← notMem_support_iff]
        exact m.notMem_support_of_degree_lt hfd
    · apply Finset.sum_congr rfl
      intro b' hb'
      rw [sPolynomial]
      obtain (⟨h, -⟩ | h) := hd b' hb' <;>
        simp [h, ← smul_eq_C_mul, smul_sub, ← mul_smul, mul_comm (m.leadingCoeff (g b'))]

Premises used: MvPolynomial.notMem_support_iff, Finset.sum_ite_eq', MonomialOrder.leadingCoeff, MonomialOrder.sPolynomial_self, Function.Injective.eq_iff, smul_zero, Insert.insert, Finset.mem_insert, forall_eq_or_imp, zero_add, smul_sub, zero_smul, AddEquiv.injective, MvPolynomial.coeff_add, reduceIte, MonomialOrder.notMem_support_of_degree_lt, ite_smul, MvPolynomial.smul_eq_C_mul, or_false, add_eq_zero_iff_neg_eq', add_zero, MonomialOrder.sPolynomial, Finset.sum_congr, SemigroupAction.mul_smul, rfl, MonomialOrder.toSyn, MvPolynomial.coeff_sum