-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
simp_rw :
  (Finsupp.sum p fun (m₁ : A) (r₁ : R) ↦
      Finsupp.sum q fun (m₂ : A) (r₂ : R) ↦ if m₁ + m₂ = ap + aq then r₁ * r₂ else 0) =
    HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
simp_rw₁ :
  (∑ x ∈ p.support,
      ∑ x_1 ∈ q.support,
        if x + x_1 = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) x : R) ((q : (a : A) → R) x_1 : R)
        else 0) =
    HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
h₀ :
  ∀ b ∈ q.support,
    b ≠ aq →
      (if ap + b = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) b : R)
        else 0) =
        0
h₁ :
  aq ∉ q.support →
    (if ap + aq = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
      else 0) =
      0
h₂ :
  ∀ b ∈ p.support,
    b ≠ ap →
      Eq.{u_1 + 1} (α := R)
        (∑ x ∈ q.support,
          if b + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) b : R) ((q : (a : A) → R) x : R)
          else 0)
        0
h₃ :
  ap ∉ p.support →
    Eq.{u_1 + 1} (α := R)
      (∑ x ∈ q.support,
        if ap + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) x : R)
        else 0)
      0
h₄ :
  aq ∉ q.support →
    (if ap + aq = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
      else 0) =
      0
h₅ :
  ∀ b ∈ p.support,
    b ≠ ap →
      Eq.{u_1 + 1} (α := R)
        (∑ x ∈ q.support,
          if b + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) b : R) ((q : (a : A) → R) x : R)
          else 0)
        0
h₆ :
  ap ∉ p.support →
    Eq.{u_1 + 1} (α := R)
      (∑ x ∈ q.support,
        if ap + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) x : R)
        else 0)
      0
h₇ :
  ∀ b ∈ p.support,
    b ≠ ap →
      Eq.{u_1 + 1} (α := R)
        (∑ x ∈ q.support,
          if b + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) b : R) ((q : (a : A) → R) x : R)
          else 0)
        0
h₈ h₉ :
  ap ∉ p.support →
    Eq.{u_1 + 1} (α := R)
      (∑ x ∈ q.support,
        if ap + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) x : R)
        else 0)
      0
⊢ (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)

Tactic:
classical
  simp_rw [mul_apply, Finsupp.sum]
  rw [Finset.sum_eq_single ap, Finset.sum_eq_single aq, if_pos rfl]
  · refine fun a ha hne => if_neg (fun he => ?_)
    apply_fun D at he; simp_rw [hadd] at he
    exact (add_lt_add_right (((Finset.le_sup ha).trans hq).lt_of_ne <| hD.ne_iff.2 hne) _).ne he
  · intro h; rw [if_pos rfl, Finsupp.notMem_support_iff.1 h, mul_zero]
  · refine fun a ha hne => Finset.sum_eq_zero (fun a' ha' => if_neg <| fun he => ?_)
    apply_fun D at he
    simp_rw [hadd] at he
    have := addLeftMono_of_addLeftStrictMono B
    exact (add_lt_add_of_lt_of_le (((Finset.le_sup ha).trans hp).lt_of_ne <| hD.ne_iff.2 hne)
      <| (Finset.le_sup ha').trans hq).ne he
  · refine fun h => Finset.sum_eq_zero (fun a _ => ite_eq_right_iff.mpr <| fun _ => ?_)
    rw [Finsupp.notMem_support_iff.mp h, zero_mul]

Premises used: Iff.mpr, AddMonoidAlgebra.mul_apply, MulZeroClass.zero_mul, Finset.sum_eq_zero, Finsupp.sum, if_pos, Finset.sum_eq_single, MulZeroClass.mul_zero, ite_eq_right_iff, if_neg, rfl