-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : AddMonoid ι
inst_5 : SetLike.GradedMonoid A
inst_6 : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
simp_rw simp_rw₁ :
  Eq.{u_4 + 1} (α := R)
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r',
      (↑(((((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (x.1 + x.2) : ↥(A (x.1 + x.2)) →+ ⨁ (i : ι), ↥(A i)) :
                    (a : ↥(A (x.1 + x.2))) → ⨁ (i : ι), ↥(A i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ x.1 x.2
                    ((r : (a : ι) → ↥(A a)) x.1 : ↥(A x.1)) ((r' : (a : ι) → ↥(A a)) x.2 : ↥(A x.2))) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R))
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' with
      x.1 + x.2 = n, (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R))
simp_rw₂ :
  Eq.{u_4 + 1} (α := R)
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r',
      (↑(if x.1 + x.2 = n then
              @GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ x.1 x.2
                ((r : (a : ι) → ↥(A a)) x.1 : ↥(A x.1)) ((r' : (a : ι) → ↥(A a)) x.2 : ↥(A x.2))
            else 0 :
            ↥(A (x.1 + x.2))) :
        R))
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' with
      x.1 + x.2 = n, (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R))
simp_rw₃ :
  Eq.{u_4 + 1} (α := R)
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r',
      if x.1 + x.2 = n then
        (↑(@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ x.1 x.2
                ((r : (a : ι) → ↥(A a)) x.1 : ↥(A x.1)) ((r' : (a : ι) → ↥(A a)) x.2 : ↥(A x.2)) :
              ↥(A (x.1 + x.2))) :
          R)
      else (↑0 : R))
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' with
      x.1 + x.2 = n, (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R))
⊢ Eq.{u_4 + 1} (α := R)
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r',
      (↑(((((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (i.1 + i.2) : ↥(A (i.1 + i.2)) →+ ⨁ (i : ι), ↥(A i)) :
                    (a : ↥(A (i.1 + i.2))) → ⨁ (i : ι), ↥(A i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ i.1 i.2
                    ((r : (a : ι) → ↥(A a)) i.1 : ↥(A i.1)) ((r' : (a : ι) → ↥(A a)) i.2 : ↥(A i.2))) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R))
    (∑ ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' with
      ij.1 + ij.2 = n, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R))
have simp_rw₄ : Eq.{u_4 + 1} (α := R)
  (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r',
    if x.1 + x.2 = n then
      (↑(@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ x.1 x.2
              ((r : (a : ι) → ↥(A a)) x.1 : ↥(A x.1)) ((r' : (a : ι) → ↥(A a)) x.2 : ↥(A x.2)) :
            ↥(A (x.1 + x.2))) :
        R)
    else 0)
  (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' with
    x.1 + x.2 = n, (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R))
Tactic: simp_rw [coe_of_apply, apply_ite, ZeroMemClass.coe_zero, ← Finset.sum_filter, SetLike.coe_gMul]