-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : (↑p : ℕ∞) ≤ weightedOrder w f
hg : (↑q : ℕ∞) ≤ weightedOrder w g
h :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          ((weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) :
            MvPowerSeries σ R) :
        R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
            ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
            ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)) :
        R)
h₁ :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q then (coeff d : (a : MvPowerSeries σ R) → R) (f * g) else 0 : R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
            ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
            ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)) :
        R)
pos :
  ∀ (d : σ →₀ ℕ) (hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
            ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
            ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)) :
        R)
neg neg₁ :
  ∀ (d : σ →₀ ℕ) (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R) (0 : R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
            ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
            ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)) :
        R)
⊢ (weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
      ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)

Tactic:
classical
  ext d
  rw [coeff_weightedHomogeneousComponent]
  split_ifs with hd
  · apply Finset.sum_congr rfl
    intro x hx
    rw [Finset.mem_antidiagonal] at hx
    rw [← hx, map_add] at hd
    simp only [coeff_weightedHomogeneousComponent]
    rcases trichotomy_of_add_eq_add hd with h | h | h
    · rw [if_pos h.1, if_pos h.2]
    · rw [if_neg (ne_of_lt h), zero_mul]
      rw [← ENat.coe_lt_coe] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hf), zero_mul]
    · rw [if_neg (ne_of_lt h), mul_zero]
      rw [← ENat.coe_lt_coe] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]
  · symm
    apply IsWeightedHomogeneous.coeff_eq_zero _ hd
    exact IsWeightedHomogeneous.mul
      (isWeightedHomogeneous_weightedHomogeneousComponent w f p)
      (isWeightedHomogeneous_weightedHomogeneousComponent w g q)

Premises used: MulZeroClass.zero_mul, map_add, MvPowerSeries.IsWeightedHomogeneous.mul, MvPowerSeries.coeff_weightedHomogeneousComponent, MulZeroClass.mul_zero, Finset.HasAntidiagonal.mem_antidiagonal, ENat.coe_lt_coe, MvPowerSeries.isWeightedHomogeneous_weightedHomogeneousComponent, Finset.sum_congr, rfl