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

State before:
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝ : AddCommMonoid β
f g : α →₀ β
h : α → γ
⊢ sumRange (mapDomain h f) = sumRange f
Tactic:
simp [sumRange, ← mapDomain_comp]
State after:
no goals