Theorem: Finsupp.sumRange_eq_sum (Etch/Verification/FinsuppLemmas.lean)

State before:
α : Type u_2
β : Type u_1
γ : Type ?u.8099
inst✝ : AddCommMonoid β
f g : α →₀ β
⊢ sumRange f = sum f fun x v => v
Tactic:
simp [sumRange, mapDomain]
State after:
no goals