Theorem: Finset.sum_univ_eq_single (GlimpseOfLean/Library/Basic.lean)

State before:
β : Type u
α : Type v
inst✝¹ : Fintype α
inst✝ : AddCommMonoid β
f : α → β
a : α
h : ∀ (b : α), b ≠ a → f b = 0
⊢ ∑ x : α, f x = f a
Tactic:
rw [Finset.sum_eq_single]
State after:
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

State before:
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
Tactic:
tauto
State after:
no goals

State before:
case h₁
β : Type u
α : Type v
inst✝¹ : Fintype α
inst✝ : AddCommMonoid β
f : α → β
a : α
h : ∀ (b : α), b ≠ a → f b = 0
⊢ a ∉ univ → f a = 0
Tactic:
exact λ ha ↦ (ha <| Finset.mem_univ a).elim
State after:
no goals