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

State before:
α : Type u_2
β : Type u_1
γ : Type ?u.14307
inst✝ : AddCommMonoid β
f g : α →₀ β
x : α
y : β
⊢ (sumRange fun₀ | x => y) = y
Tactic:
simp [sumRange]
State after:
no goals