no goals
α : Type u_2
β : Type ?u.60897
γ : Type ?u.60900
ι : Sort u_1
inst✝¹ : ConditionallyCompleteLattice α
s t : Set α
a b : α
inst✝ : Nonempty ι
f : ι → α
h₁ : ∀ (i : ι), b ≤ f i
h₂ : ∀ (w : α), b < w → ∃ i, f i < w
⊢ (⨅ (i : ι), f i) = b
exact @ciSup_eq_of_forall_le_of_forall_lt_exists_gt αᵒᵈ _ _ _ _ ‹_› ‹_› ‹_›