no goals
α : Type u_1
β : Type ?u.75412
β₂ : Type ?u.75415
γ : Type ?u.75418
ι : Sort u_2
ι' : Sort ?u.75424
κ : ι → Sort u_3
κ' : ι' → Sort ?u.75434
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : (i : ι) → κ i → α
⊢ (a ≤ ⨅ (i : ι) (j : κ i), f i j) ↔ ∀ (i : ι) (j : κ i), a ≤ f i j
simp_rw [le_iInf_iff]