Theorem: DirectSum.coeLinearMap_eq_dfinsupp_sum (DividedPowers/ForMathlib/GradedAlgebra.lean)

State before:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u
inst✝¹ : Semiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
⊢ (coeLinearMap A) x = DFinsupp.sum x fun i x => ↑x
Tactic:
simp only [coeLinearMap, toModule, DFinsupp.lsum, LinearEquiv.coe_mk, LinearMap.coe_mk,
  AddHom.coe_mk]
State after:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u
inst✝¹ : Semiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => (A i).subtype.toAddMonoidHom) x = DFinsupp.sum x fun i x => ↑x

State before:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u
inst✝¹ : Semiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => (A i).subtype.toAddMonoidHom) x = DFinsupp.sum x fun i x => ↑x
Tactic:
rw [DFinsupp.sumAddHom_apply]
State after:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u
inst✝¹ : Semiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sum x fun x => ⇑(A x).subtype.toAddMonoidHom) = DFinsupp.sum x fun i x => ↑x

State before:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u
inst✝¹ : Semiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sum x fun x => ⇑(A x).subtype.toAddMonoidHom) = DFinsupp.sum x fun i x => ↑x
Tactic:
simp only [LinearMap.toAddMonoidHom_coe, Submodule.coeSubtype]
State after:
no goals