no goals
α : Type u_1
ι : Sort ?u.12832
κ : ι → Sort ?u.12837
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
u : β → α
l : LowerAdjoint u
l₁ : α → β
gc'✝¹ : GaloisConnection l₁ u
l₂ : α → β
gc'✝ : GaloisConnection l₂ u
h : { toFun := l₁, gc' := gc'✝¹ }.toFun = { toFun := l₂, gc' := gc'✝ }.toFun
⊢ { toFun := l₁, gc' := gc'✝¹ } = { toFun := l₂, gc' := gc'✝ }
congr