rw [iInf_le_iff]
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ ⨅ x ∈ s, f x ≤ b ↔ ∀ (b' : β), (∀ x ∈ s, b' ≤ f x) → b' ≤ b
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
⊢ (∀ (b_1 : β), (∀ (i : α), b_1 ≤ ⨅ (_ : i ∈ s), f i) → b_1 ≤ b) ↔ ∀ (b' : β), (∀ x ∈ s, b' ≤ f x) → b' ≤ b