no goals
F : Type ?u.215549
α : Type u_1
β : Type ?u.215555
γ : Type ?u.215558
ι : Type u_2
κ : Type ?u.215564
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : ¬c ∈ t
⊢ ((∀ (b : ι), b ∈ t → f b < a) → sup t f < a) → (∀ (b : ι), b ∈ cons c t hc → f b < a) → sup (cons c t hc) f < a
simpa only [sup_cons, sup_lt_iff, mem_cons, forall_eq_or_imp] using And.imp_right