no goals
α : Type u_2
β : Type ?u.102664
β₂ : Type ?u.102667
γ : Type ?u.102670
ι : Sort u_1
ι' : Sort ?u.102676
κ : ι → Sort ?u.102681
κ' : ι' → Sort ?u.102686
inst✝¹ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (a ⊓ ⨅ (x : ι), f x) = ⨅ (x : ι), a ⊓ f x
rw [iInf_inf_eq, iInf_const]