no goals
ι : Type u_2
α : Type ?u.187623
β : Type ?u.187626
M : Type u_1
N : Type ?u.187632
G : Type ?u.187635
k : Type ?u.187638
R : Type ?u.187641
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i in s, f i = ⊤ ↔ ∃ i, i ∈ s ∧ f i = ⊤
induction s using Finset.cons_induction <;> simp [*]