no goals
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort ?u.42456
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
f : ι → α
hf : ∀ (i : ι), u (l (f i)) = f i
⊢ l (⨅ (i : ι), f i) = l (⨅ (i : ι), u (l (f i)))
simp [hf]