obtain (ht | hne) := eq_or_ne (f a) ⊤
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
ht : f a = ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤

case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Finite
a : α
s' : Set α
has' : a ∉ s'
x✝ : s'.Finite
IH : ∑' (x : ↑s'), f ↑x = ⊤ → ∃ a ∈ s', f a = ⊤
htop : ∑' (x : ↑(insert a s')), f ↑x = ⊤
hne : f a ≠ ⊤
⊢ ∃ a_1 ∈ insert a s', f a_1 = ⊤