no goals
ι : Type u_2
α : Type ?u.191723
β : Type ?u.191726
M : Type u_1
N : Type ?u.191732
G : Type ?u.191735
k : Type ?u.191738
R : Type ?u.191741
inst✝¹ : AddCommMonoid M
inst✝ : LT M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i in s, f i < ⊤ ↔ ∀ (i : ι), i ∈ s → f i < ⊤
simp only [WithTop.lt_top_iff_ne_top, ne_eq, sum_eq_top_iff, not_exists, not_and]