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

State before:
ι : Type v
inst✝⁴ : DecidableEq ι
M✝ : Type w
inst✝³ : DecidableEq M✝
inst✝² : AddCommMonoid M✝
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
⊢ (DirectSum.coeAddMonoidHom A) x = DFinsupp.sum x fun i x => ↑x
Tactic:
simp only [DirectSum.coeAddMonoidHom, DirectSum.toAddMonoid,
  DFinsupp.liftAddHom, AddEquiv.coe_mk, Equiv.coe_fn_mk]
State after:
ι : Type v
inst✝⁴ : DecidableEq ι
M✝ : Type w
inst✝³ : DecidableEq M✝
inst✝² : AddCommMonoid M✝
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => AddSubmonoidClass.subtype (A i)) x = DFinsupp.sum x fun i x => ↑x

State before:
ι : Type v
inst✝⁴ : DecidableEq ι
M✝ : Type w
inst✝³ : DecidableEq M✝
inst✝² : AddCommMonoid M✝
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => AddSubmonoidClass.subtype (A i)) x = DFinsupp.sum x fun i x => ↑x
Tactic:
exact DFinsupp.sumAddHom_apply _ x
State after:
no goals