-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
rw :
  (AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) (x • y) =
    HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i)) ((RingHom.id A : (a : A) → A) x : A)
      ((AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i))
rw₁ :
  (AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
      (HSMul.hSMul.{u_4, u_5, u_5} (α := A)
        (∑ i ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
          (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A))
        y) =
    HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i))
      ((RingHom.id A : (a : A) → A)
          (∑ i ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
            (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)) :
        A)
      ((AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i))
⊢ AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (x • y) =
    HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i)) ((RingHom.id A : (a : A) → A) x : A)
      (AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) y)
have rw₂ : (AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
    (HSMul.hSMul.{u_4, u_5, u_5} (α := A)
      (∑ i ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
        (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A))
      y) =
  HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
      (RingHom.id A : (a : A) → A)
        (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) x_1) : A))
    ((AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i))
Tactic: classical
  rw [AddHom.toFun_eq_coe, ← DirectSum.sum_support_decompose 𝓐 x, map_sum, Finset.sum_smul,
    AddEquiv.coe_toAddHom, map_sum, Finset.sum_smul]
  refine Finset.sum_congr rfl (fun i _hi => ?_)
  rw [RingHom.id_apply, ← DirectSum.sum_support_decompose 𝓜 y, map_sum, Finset.smul_sum, map_sum,
    Finset.smul_sum]
  refine Finset.sum_congr rfl (fun j _hj => ?_)
  rw [show (decompose 𝓐 x i : A) • (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j) : (⨁ i, 𝓜 i)) =
    DirectSum.Gmodule.smulAddMonoidHom _ _ (decompose 𝓐 ↑(decompose 𝓐 x i))
    (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j)) from DirectSum.Gmodule.smul_def _ _ _ _]
  simp only [decomposeAddEquiv_apply, decompose_coe, Gmodule.smulAddMonoidHom_apply_of_of]
  convert! DirectSum.decompose_coe 𝓜 _
  rfl