F : Type ?u.302432
α : Type u_1
β : Type ?u.302438
γ : Type ?u.302441
ι : Type u_2
κ : Type ?u.302447
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.302432
α : Type u_1
β : Type ?u.302438
γ : Type ?u.302441
ι : Type u_2
κ : Type ?u.302447
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ a < sup' s H f ↔ ∃ b, b ∈ s ∧ a < f b
rw [← WithBot.coe_lt_coe, coe_sup', Finset.lt_sup_iff]
no goals
F : Type ?u.302432
α : Type u_1
β : Type ?u.302438
γ : Type ?u.302441
ι : Type u_2
κ : Type ?u.302447
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_lt_coe)