Lean4
/-- Lift the infima along a Galois insertion -/
abbrev liftSemilatticeInf [SemilatticeInf α] (gi : GaloisInsertion l u) : SemilatticeInf β :=
{
‹PartialOrder
β› with
inf := fun a b =>
gi.choice (u a ⊓ u b) <|
le_inf (gi.gc.monotone_u <| gi.gc.l_le <| inf_le_left) (gi.gc.monotone_u <| gi.gc.l_le <| inf_le_right)
inf_le_left := by simp only [gi.choice_eq]; exact fun a b => gi.gc.l_le inf_le_left
inf_le_right := by simp only [gi.choice_eq]; exact fun a b => gi.gc.l_le inf_le_right
le_inf := by
simp only [gi.choice_eq]
exact fun a b c hac hbc =>
(gi.le_l_u a).trans <| gi.gc.monotone_l <| le_inf (gi.gc.monotone_u hac) (gi.gc.monotone_u hbc) }
-- See note [reducible non-instances]