[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
i j : ι
x : A i
y : M j
⊢ ↑(↑(smulAddMonoidHom A M) (↑(of A i) x)) (↑(of M j) y) = ↑(of M (i + j)) (GSmul.smul x y)
[PROOFSTEP]
simp [smulAddMonoidHom]
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ 1 • x = x
[PROOFSTEP]
suffices smulAddMonoidHom A M 1 = AddMonoidHom.id (⨁ i, M i) from FunLike.congr_fun this x
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ ↑(smulAddMonoidHom A M) 1 = AddMonoidHom.id (⨁ (i : ι), M i)
[PROOFSTEP]
apply DirectSum.addHom_ext
[GOAL]
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ ∀ (i : ι) (y : M i),
    ↑(↑(smulAddMonoidHom A M) 1) (↑(of (fun i => M i) i) y) =
      ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) y)
[PROOFSTEP]
intro i xi
[GOAL]
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(↑(smulAddMonoidHom A M) 1) (↑(of (fun i => M i) i) xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
[PROOFSTEP]
rw [show (1 : DirectSum ι fun i => A i) = (of A 0) GOne.one by rfl]
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ 1 = ↑(of A 0) GOne.one
[PROOFSTEP]
rfl
[GOAL]
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(↑(smulAddMonoidHom A M) (↑(of A 0) GOne.one)) (↑(of (fun i => M i) i) xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
[PROOFSTEP]
rw [smulAddMonoidHom_apply_of_of]
[GOAL]
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(of M (0 + i)) (GSmul.smul GOne.one xi) = ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
[PROOFSTEP]
exact
  DirectSum.of_eq_of_gradedMonoid_eq
    (one_smul (GradedMonoid A) <| GradedMonoid.mk i xi)
      -- Porting note: renamed to mul_smul' since DirectSum.Gmodule.mul_smul already exists
      -- Almost identical to the proof of `direct_sum.mul_assoc`
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ι), A i
c : ⨁ (i : ι), M i
⊢ (a * b) • c = a • b • c
[PROOFSTEP]
suffices
  (
          -- `fun a b c ↦ (a * b) • c` as a bundled homsmulAddMonoidHom A M).compHom.comp
      (DirectSum.mulHom A) =
    (AddMonoidHom.compHom AddMonoidHom.flipHom <| (smulAddMonoidHom A M).flip.compHom.comp <| smulAddMonoidHom A M).flip
  from
  -- `fun a b c ↦ a • (b • c)` as a bundled homFunLike.congr_fun (FunLike.congr_fun (FunLike.congr_fun this a) b) c
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ι), A i
c : ⨁ (i : ι), M i
⊢ comp (↑compHom (smulAddMonoidHom A M)) (mulHom A) =
    AddMonoidHom.flip
      (↑(↑compHom flipHom) (comp (↑compHom (AddMonoidHom.flip (smulAddMonoidHom A M))) (smulAddMonoidHom A M)))
[PROOFSTEP]
ext ai ax bi bx ci cx : 6
[GOAL]
case H.h.H.h.H.h
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ι), A i
c : ⨁ (i : ι), M i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : M ci
⊢ ↑(comp
          (↑(comp (↑(comp (comp (↑compHom (smulAddMonoidHom A M)) (mulHom A)) (of (fun i => A i) ai)) ax)
                (of (fun i => A i) bi))
            bx)
          (of (fun i => M i) ci))
      cx =
    ↑(comp
          (↑(comp
                (↑(comp
                      (AddMonoidHom.flip
                        (↑(↑compHom flipHom)
                          (comp (↑compHom (AddMonoidHom.flip (smulAddMonoidHom A M))) (smulAddMonoidHom A M))))
                      (of (fun i => A i) ai))
                  ax)
                (of (fun i => A i) bi))
            bx)
          (of (fun i => M i) ci))
      cx
[PROOFSTEP]
dsimp only [coe_comp, Function.comp_apply, compHom_apply_apply, flip_apply, flipHom_apply]
[GOAL]
case H.h.H.h.H.h
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ι), A i
c : ⨁ (i : ι), M i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : M ci
⊢ ↑(↑(smulAddMonoidHom A M) (↑(↑(mulHom A) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) bi) bx)))
      (↑(of (fun i => M i) ci) cx) =
    ↑(↑(smulAddMonoidHom A M) (↑(of (fun i => A i) ai) ax))
      (↑(↑(smulAddMonoidHom A M) (↑(of (fun i => A i) bi) bx)) (↑(of (fun i => M i) ci) cx))
[PROOFSTEP]
rw [smulAddMonoidHom_apply_of_of, smulAddMonoidHom_apply_of_of, DirectSum.mulHom_of_of, smulAddMonoidHom_apply_of_of]
[GOAL]
case H.h.H.h.H.h
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ι), A i
c : ⨁ (i : ι), M i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : M ci
⊢ ↑(of M (ai + bi + ci)) (GSmul.smul (GMul.mul ax bx) cx) = ↑(of M (ai + (bi + ci))) (GSmul.smul ax (GSmul.smul bx cx))
[PROOFSTEP]
exact
  DirectSum.of_eq_of_gradedMonoid_eq (mul_smul (GradedMonoid.mk ai ax) (GradedMonoid.mk bi bx) (GradedMonoid.mk ci cx))
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
r s : ⨁ (i : ι), A i
x : ⨁ (i : ι), M i
⊢ (r + s) • x = r • x + s • x
[PROOFSTEP]
simp only [smul_def, map_add, AddMonoidHom.add_apply]
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ 0 • x = 0
[PROOFSTEP]
simp only [smul_def, map_zero, AddMonoidHom.zero_apply]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
⊢ Module A (⨁ (i : ι), { x // x ∈ 𝓜 i })
[PROOFSTEP]
letI := isModule 𝓐 𝓜
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
this : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
⊢ Module A (⨁ (i : ι), { x // x ∈ 𝓜 i })
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
⊢ M ≃ₗ[A] ⨁ (i : ι), { x // x ∈ 𝓜 i }
[PROOFSTEP]
letI h := isModule 𝓐 𝓜
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
⊢ M ≃ₗ[A] ⨁ (i : ι), { x // x ∈ 𝓜 i }
[PROOFSTEP]
refine
  ⟨⟨(DirectSum.decomposeAddEquiv 𝓜).toAddHom, ?_⟩, (DirectSum.decomposeAddEquiv 𝓜).symm.toFun,
    (DirectSum.decomposeAddEquiv 𝓜).left_inv, (DirectSum.decomposeAddEquiv 𝓜).right_inv⟩
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
⊢ ∀ (r : A) (x : M),
    AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (r • x) =
      ↑(RingHom.id A) r • AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) x
[PROOFSTEP]
intro x y
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
⊢ AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (x • y) =
    ↑(RingHom.id A) x • AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) y
[PROOFSTEP]
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, Equiv.invFun_as_coe, Equiv.symm_symm, decompose_coe,
  Gmodule.smulAddMonoidHom_apply_of_of]
convert DirectSum.decompose_coe 𝓜 _
rfl
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
⊢ AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (x • y) =
    ↑(RingHom.id A) x • AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) y
[PROOFSTEP]
rw [AddHom.toFun_eq_coe, ← DirectSum.sum_support_decompose 𝓐 x, map_sum, Finset.sum_smul, AddEquiv.coe_toAddHom,
  map_sum, Finset.sum_smul]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
⊢ ∑ x_1 in DFinsupp.support (↑(decompose 𝓐) x), ↑(decomposeAddEquiv 𝓜) (↑(↑(↑(decompose 𝓐) x) x_1) • y) =
    ∑ i in DFinsupp.support (↑(decompose 𝓐) x), ↑(RingHom.id A) ↑(↑(↑(decompose 𝓐) x) i) • ↑(decomposeAddEquiv 𝓜) y
[PROOFSTEP]
refine Finset.sum_congr rfl (fun i _hi => ?_)
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
⊢ ↑(decomposeAddEquiv 𝓜) (↑(↑(↑(decompose 𝓐) x) i) • y) =
    ↑(RingHom.id A) ↑(↑(↑(decompose 𝓐) x) i) • ↑(decomposeAddEquiv 𝓜) y
[PROOFSTEP]
rw [RingHom.id_apply, ← DirectSum.sum_support_decompose 𝓜 y, map_sum, Finset.smul_sum, map_sum, Finset.smul_sum]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
⊢ ∑ x_1 in DFinsupp.support (↑(decompose 𝓜) y),
      ↑(decomposeAddEquiv 𝓜) (↑(↑(↑(decompose 𝓐) x) i) • ↑(↑(↑(decompose 𝓜) y) x_1)) =
    ∑ x_1 in DFinsupp.support (↑(decompose 𝓜) y),
      ↑(↑(↑(decompose 𝓐) x) i) • ↑(decomposeAddEquiv 𝓜) ↑(↑(↑(decompose 𝓜) y) x_1)
[PROOFSTEP]
refine Finset.sum_congr rfl (fun j _hj => ?_)
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
j : ι
_hj : j ∈ DFinsupp.support (↑(decompose 𝓜) y)
⊢ ↑(decomposeAddEquiv 𝓜) (↑(↑(↑(decompose 𝓐) x) i) • ↑(↑(↑(decompose 𝓜) y) j)) =
    ↑(↑(↑(decompose 𝓐) x) i) • ↑(decomposeAddEquiv 𝓜) ↑(↑(↑(decompose 𝓜) y) j)
[PROOFSTEP]
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 _ _ _ _]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
j : ι
_hj : j ∈ DFinsupp.support (↑(decompose 𝓜) y)
⊢ ↑(decomposeAddEquiv 𝓜) (↑(↑(↑(decompose 𝓐) x) i) • ↑(↑(↑(decompose 𝓜) y) j)) =
    ↑(↑(Gmodule.smulAddMonoidHom (fun i => { x // x ∈ 𝓐 i }) fun i => { x // x ∈ 𝓜 i })
          (↑(decompose 𝓐) ↑(↑(↑(decompose 𝓐) x) i)))
      (↑(decomposeAddEquiv 𝓜) ↑(↑(↑(decompose 𝓜) y) j))
[PROOFSTEP]
simp only [decomposeAddEquiv_apply, Equiv.invFun_as_coe, Equiv.symm_symm, decompose_coe,
  Gmodule.smulAddMonoidHom_apply_of_of]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
j : ι
_hj : j ∈ DFinsupp.support (↑(decompose 𝓜) y)
⊢ ↑(decompose 𝓜) (↑(↑(↑(decompose 𝓐) x) i) • ↑(↑(↑(decompose 𝓜) y) j)) =
    ↑(of (fun i => { x // x ∈ 𝓜 i }) (i + j)) (GradedMonoid.GSmul.smul (↑(↑(decompose 𝓐) x) i) (↑(↑(decompose 𝓜) y) j))
[PROOFSTEP]
convert DirectSum.decompose_coe 𝓜 _
[GOAL]
case h.e'_2.h.e'_6
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
j : ι
_hj : j ∈ DFinsupp.support (↑(decompose 𝓜) y)
⊢ ↑(↑(↑(decompose 𝓐) x) i) • ↑(↑(↑(decompose 𝓜) y) j) =
    ↑(GradedMonoid.GSmul.smul (↑(↑(decompose 𝓐) x) i) (↑(↑(decompose 𝓜) y) j))
[PROOFSTEP]
rfl
