awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.GradedModule
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 :
  Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
      (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) x_1) : A) • y))
    (∑ i ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
      HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i))
        ((RingHom.id A : (a : A) → A)
            (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) :
          A)
        ((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)

Tactic:
rw [AddHom.toFun_eq_coe, ← DirectSum.sum_support_decompose 𝓐 x, map_sum, Finset.sum_smul,
    AddEquiv.coe_toAddHom, map_sum, Finset.sum_smul]

Premises used: Finset.sum_smul, AddHom.toFun_eq_coe, map_sum, DirectSum.sum_support_decompose, AddEquiv.coe_toAddHom
-- Module: Mathlib.Algebra.Module.GradedModule
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
⊢ Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
      (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) x_1) : A) • y))
    (∑ i ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
      HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i))
        ((RingHom.id A : (a : A) → A)
            (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) :
          A)
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)))

Tactic:
Finset.sum_congr rfl (fun i _hi => ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Module.GradedModule
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
refine :
  ∀ (i : ιA)
    (_hi :
      Membership.mem (γ := Finset ιA)
        (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i),
    (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((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)
            (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) :
          A)
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i))
⊢ Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
      (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) x_1) : A) • y))
    (∑ i ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
      HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i))
        ((RingHom.id A : (a : A) → A)
            (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) :
          A)
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)))

Tactic:
refine Finset.sum_congr rfl (fun i _hi => ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Module.GradedModule
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
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
rw :
  Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y),
      (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) x_1) : M)))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y),
      HSMul.hSMul (β := ⨁ (i : ιM), ↥(𝓜 i))
        (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
            (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) x_1) : M) :
          ⨁ (i : ιM), ↥(𝓜 i)))
⊢ (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
      ((↑((((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)
          (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) :
        A)
      ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i))

Tactic:
rw [RingHom.id_apply, ← DirectSum.sum_support_decompose 𝓜 y, map_sum, Finset.smul_sum, map_sum,
    Finset.smul_sum]

Premises used: RingHom.id_apply, map_sum, Finset.smul_sum, DirectSum.sum_support_decompose
-- Module: Mathlib.Algebra.Module.GradedModule
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
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
⊢ Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y),
      (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) x_1) : M)))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y),
      HSMul.hSMul (β := ⨁ (i : ιM), ↥(𝓜 i))
        (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
            (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) x_1) : M) :
          ⨁ (i : ιM), ↥(𝓜 i)))

Tactic:
Finset.sum_congr rfl (fun j _hj => ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Module.GradedModule
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
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
refine :
  ∀ (j : ιM)
    (_hj :
      Membership.mem (γ := Finset ιM)
        (DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y)) j),
    (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) =
      HSMul.hSMul (β := ⨁ (i : ιM), ↥(𝓜 i))
        (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
            (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M) :
          ⨁ (i : ιM), ↥(𝓜 i))
⊢ Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y),
      (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) x_1) : M)))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y),
      HSMul.hSMul (β := ⨁ (i : ιM), ↥(𝓜 i))
        (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
            (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) x_1) : M) :
          ⨁ (i : ιM), ↥(𝓜 i)))

Tactic:
refine Finset.sum_congr rfl (fun j _hj => ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Module.GradedModule
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
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
j : ιM
_hj :
  Membership.mem (γ := Finset ιM)
    (DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y)) j
rw :
  Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
      ⨁ (i : ιM), ↥(𝓜 i))
    ((((Gmodule.smulAddMonoidHom (fun (i : ιA) ↦ ↥(𝓐 i)) fun (i : ιM) ↦ ↥(𝓜 i) :
                (a : ⨁ (i : ιA), ↥(𝓐 i)) → (⨁ (i : ιM), ↥(𝓜 i)) →+ ⨁ (i : ιM), ↥(𝓜 i))
              ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i))
                (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) :
                  A)) :
            (⨁ (i : ιM), ↥(𝓜 i)) →+ ⨁ (i : ιM), ↥(𝓜 i)) :
          (a : ⨁ (i : ιM), ↥(𝓜 i)) → ⨁ (i : ιM), ↥(𝓜 i))
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
      ⨁ (i : ιM), ↥(𝓜 i))
⊢ (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
      ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
        (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) =
    HSMul.hSMul (β := ⨁ (i : ιM), ↥(𝓜 i))
      (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)
      ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M) :
        ⨁ (i : ιM), ↥(𝓜 i))

Tactic:
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 _ _ _ _]

Premises used: DirectSum.decomposeAddEquiv, Membership.mem, Subtype, Subtype.val, DFunLike.coe, DirectSum.Gmodule.smul_def, DirectSum.decompose
-- Module: Mathlib.Algebra.Module.GradedModule
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
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
j : ιM
_hj :
  Membership.mem (γ := Finset ιM)
    (DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y)) j
simp :
  Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
      ⨁ (i : ιM), ↥(𝓜 i))
    (((of.{u_2, u_5} (fun (i : ιM) ↦ ↥(𝓜 i)) (i +ᵥ j) : ↥(𝓜 (i +ᵥ j)) →+ ⨁ (i : ιM), ↥(𝓜 i)) :
          (a : ↥(𝓜 (i +ᵥ j))) → ⨁ (i : ιM), ↥(𝓜 i))
        (@GradedMonoid.GSMul.smul _ _ (fun (i : ιA) ↦ ↥(𝓐 i)) (fun (i : ιM) ↦ ↥(𝓜 i))
          (@AddSemigroupAction.toVAdd _ _ AddMonoid.toAddSemigroup _) _ _ _
          ((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i)
          ((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j)) :
      ⨁ (i : ιM), ↥(𝓜 i))
⊢ Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
      ⨁ (i : ιM), ↥(𝓜 i))
    ((((Gmodule.smulAddMonoidHom (fun (i : ιA) ↦ ↥(𝓐 i)) fun (i : ιM) ↦ ↥(𝓜 i) :
                (a : ⨁ (i : ιA), ↥(𝓐 i)) → (⨁ (i : ιM), ↥(𝓜 i)) →+ ⨁ (i : ιM), ↥(𝓜 i))
              ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i))
                (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) :
                  A)) :
            (⨁ (i : ιM), ↥(𝓜 i)) →+ ⨁ (i : ιM), ↥(𝓜 i)) :
          (a : ⨁ (i : ιM), ↥(𝓜 i)) → ⨁ (i : ιM), ↥(𝓜 i))
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
      ⨁ (i : ιM), ↥(𝓜 i))

Tactic:
simp only [decomposeAddEquiv_apply, decompose_coe, Gmodule.smulAddMonoidHom_apply_of_of]

Premises used: DirectSum.Gmodule.smulAddMonoidHom_apply_of_of, DirectSum.decomposeAddEquiv_apply, DirectSum.decompose_coe
-- Module: Mathlib.Algebra.Module.GradedModule
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
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
j : ιM
_hj :
  Membership.mem (γ := Finset ιM)
    (DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y)) j
⊢ Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        (↑(@GradedMonoid.GSMul.smul _ _ (fun (i : ιA) ↦ ↥(𝓐 i)) (fun (i : ιM) ↦ ↥(𝓜 i))
                (@AddSemigroupAction.toVAdd _ _ AddMonoid.toAddSemigroup _) _ _ _
                ((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i)
                ((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) :
              ↥(𝓜 (i +ᵥ j))) :
          M) :
      ⨁ (i : ιM), ↥(𝓜 i))
    (((of.{u_2, u_5} (fun (i : ιM) ↦ ↥(𝓜 i)) (i +ᵥ j) : ↥(𝓜 (i +ᵥ j)) →+ ⨁ (i : ιM), ↥(𝓜 i)) :
          (a : ↥(𝓜 (i +ᵥ j))) → ⨁ (i : ιM), ↥(𝓜 i))
        (@GradedMonoid.GSMul.smul _ _ (fun (i : ιA) ↦ ↥(𝓐 i)) (fun (i : ιM) ↦ ↥(𝓜 i))
          (@AddSemigroupAction.toVAdd _ _ AddMonoid.toAddSemigroup _) _ _ _
          ((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i)
          ((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j)) :
      ⨁ (i : ιM), ↥(𝓜 i))

Tactic:
DirectSum.decompose_coe 𝓜 _

Premises used: DirectSum.decompose_coe
-- Module: Mathlib.Algebra.Module.GradedModule
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
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
j : ιM
_hj :
  Membership.mem (γ := Finset ιM)
    (DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y)) j
h₁ :
  (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
      (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M) =
    (↑(@GradedMonoid.GSMul.smul _ _ (fun (i : ιA) ↦ ↥(𝓐 i)) (fun (i : ιM) ↦ ↥(𝓜 i))
            (@AddSemigroupAction.toVAdd _ _ AddMonoid.toAddSemigroup _) _ _ _
            ((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i)
            ((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) :
          ↥(𝓜 (i +ᵥ j))) :
      M)
⊢ Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
      ⨁ (i : ιM), ↥(𝓜 i))
    (((of.{u_2, u_5} (fun (i : ιM) ↦ ↥(𝓜 i)) (i +ᵥ j) : ↥(𝓜 (i +ᵥ j)) →+ ⨁ (i : ιM), ↥(𝓜 i)) :
          (a : ↥(𝓜 (i +ᵥ j))) → ⨁ (i : ιM), ↥(𝓜 i))
        (@GradedMonoid.GSMul.smul _ _ (fun (i : ιA) ↦ ↥(𝓐 i)) (fun (i : ιM) ↦ ↥(𝓜 i))
          (@AddSemigroupAction.toVAdd _ _ AddMonoid.toAddSemigroup _) _ _ _
          ((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i)
          ((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j)) :
      ⨁ (i : ιM), ↥(𝓜 i))

Tactic:
convert! DirectSum.decompose_coe 𝓜 _

Premises used: DirectSum.decompose_coe