awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
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
⊢ (∑ 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)
have 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
Tactic: rw [Finset.sum_eq_single ap, Finset.sum_eq_single aq, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
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
⊢ (∑ 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)
have 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
Tactic: rw [Finset.sum_eq_single ap, Finset.sum_eq_single aq, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ ∀ 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
have h₀ : ∀ (a : A) (ha : a ∈ q.support) (hne : a ≠ aq) (he : ap + a = ap + aq), False
Tactic: refine fun a ha hne => if_neg (fun he => ?_)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (hypothesis)
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
a : A
ha : a ∈ q.support
hne : a ≠ aq
he : ap + a = ap + aq
⊢ False
have he₁ : D (ap + a) = D (ap + aq)
Tactic: apply_fun D at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (hypothesis)
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
a : A
ha : a ∈ q.support
hne : a ≠ aq
he : D (ap + a) = D (ap + aq)
⊢ False
have he₁ : D ap + D a = D ap + D aq
Tactic: simp_rw [hadd] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
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
have h₁ : HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R) = 0
Tactic: rw [if_pos rfl, Finsupp.notMem_support_iff.1 h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
h : aq ∉ q.support
h₁ : HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R) = 0
⊢ (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
have h₂ : HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) (0 : R) = 0
Tactic: rw [if_pos rfl, Finsupp.notMem_support_iff.1 h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
h : aq ∉ q.support
h₁ : HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R) = 0
h₂ : HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) (0 : R) = 0
⊢ (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
have h₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [if_pos rfl, Finsupp.notMem_support_iff.1 h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ ∀ 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
have h₀ : ∀ (a : A) (ha : a ∈ p.support) (hne : a ≠ ap) (a' : A) (ha' : a' ∈ q.support) (he : a + a' = ap + aq), False
Tactic: refine fun a ha hne => Finset.sum_eq_zero (fun a' ha' => if_neg <| fun he => ?_)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (hypothesis)
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
a : A
ha : a ∈ p.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.support
he : a + a' = ap + aq
⊢ False
have he₁ : D (a + a') = D (ap + aq)
Tactic: apply_fun D at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (hypothesis)
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
a : A
ha : a ∈ p.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.support
he : D (a + a') = D (ap + aq)
⊢ False
have he₁ : D a + D a' = D ap + D aq
Tactic: simp_rw [hadd] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (hypothesis)
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
a : A
ha : a ∈ p.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.support
he : D a + D a' = D ap + D aq
⊢ False
have this : AddLeftMono B
Tactic: have := addLeftMono_of_addLeftStrictMono B
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ 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
have h₁ : ∀ (h : ap ∉ p.support),
  ∀ a ∈ q.support,
    ap + a = ap + aq → HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) a : R) = 0
Tactic: refine fun h => Finset.sum_eq_zero (fun a _ => ite_eq_right_iff.mpr <| fun _ => ?_)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
h : ap ∉ p.support
a : A
h_1 : a ∈ q.support
h_2 : ap + a = ap + aq
⊢ HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) a : R) = 0
have h₁ : HMul.hMul (α := R) (β := R) (0 : R) ((q : (a : A) → R) a : R) = 0
Tactic: rw [Finsupp.notMem_support_iff.mp h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
h : ap ∉ p.support
a : A
h_1 : a ∈ q.support
h_2 : ap + a = ap + aq
h₁ : HMul.hMul (α := R) (β := R) (0 : R) ((q : (a : A) → R) a : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) a : R) = 0
have h₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [Finsupp.notMem_support_iff.mp h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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)
⊢ (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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)
⊢ (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
have 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
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]