no goals
α : Type u_1
β : Type ?u.34572
β₂ : Type ?u.34575
γ : Type ?u.34578
ι : Sort u_2
ι' : Sort ?u.34584
κ : ι → Sort ?u.34589
κ' : ι' → Sort ?u.34594
inst✝ : CompleteSemilatticeInf α
s✝ t : Set α
a b : α
s : ι → α
⊢ iInf s ≤ a ↔ ∀ (b : α), (∀ (i : ι), b ≤ s i) → b ≤ a
simp [iInf, sInf_le_iff, lowerBounds]