Theorem: DirectSum.toAddMonoid_mk (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
ι : Type u_1
inst✝³ : DecidableEq ι
R : Type u_2
inst✝² : Semiring R
β : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u_4
inst✝ : AddCommMonoid γ
ψ : (i : ι) → β i →+ γ
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
⊢ (toAddMonoid ψ) ((mk β s) x) = ∑ i ∈ s, (ψ i) (if h : i ∈ s then x ⟨i, h⟩ else 0)
Tactic:
rw [mk_eq_sum, map_sum, Finset.sum_congr rfl (fun i _ => toAddMonoid_of _ _ _)]
State after:
no goals