rw [Finset.sum_eq_single]
β : Type u
α : Type v
inst✝¹ : Fintype α
inst✝ : AddCommMonoid β
f : α → β
a : α
h : ∀ (b : α), b ≠ a → f b = 0
⊢ ∑ x : α, f x = f a
case h₀
β : Type u
α : Type v
inst✝¹ : Fintype α
inst✝ : AddCommMonoid β
f : α → β
a : α
h : ∀ (b : α), b ≠ a → f b = 0
⊢ ∀ b ∈ univ, b ≠ a → f b = 0

case h₁
β : Type u
α : Type v
inst✝¹ : Fintype α
inst✝ : AddCommMonoid β
f : α → β
a : α
h : ∀ (b : α), b ≠ a → f b = 0
⊢ a ∉ univ → f a = 0