F : Type ?u.300601
α : Type u_1
β : Type ?u.300607
γ : Type ?u.300610
ι : Type u_2
κ : Type ?u.300616
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ (∃ b, b ∈ s ∧ ↑a ≤ (WithBot.some ∘ f) b) ↔ ∃ b, b ∈ s ∧ a ≤ f b
F : Type ?u.300601
α : Type u_1
β : Type ?u.300607
γ : Type ?u.300610
ι : Type u_2
κ : Type ?u.300616
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ a ≤ sup' s H f ↔ ∃ b, b ∈ s ∧ a ≤ f b
rw [← WithBot.coe_le_coe, coe_sup', Finset.le_sup_iff (WithBot.bot_lt_coe a)]
no goals
F : Type ?u.300601
α : Type u_1
β : Type ?u.300607
γ : Type ?u.300610
ι : Type u_2
κ : Type ?u.300616
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ (∃ b, b ∈ s ∧ ↑a ≤ (WithBot.some ∘ f) b) ↔ ∃ b, b ∈ s ∧ a ≤ f b
exact exists_congr (fun _ => and_congr_right' WithBot.coe_le_coe)