feat: speed up liftSemilatticeInf and liftSemilatticeSup (#1244)

For some reason, adding `by exact` makes these declarations elaborate much more quickly. Might have something to do with the fact that the proofs elaborate to claims about `αᵒᵈᵒᵈ` and we're applying them to `α`.

Mathlib/Order/GaloisConnection.lean

@@ -859,8 +859,9 @@ section lift
 
 variable [PartialOrder α]
 
--- Porting note: In this and the following few defs, the elaborator struggled with αᵒᵈ vs α;
--- now it compiles but much slower than in mathlib3.
+-- Porting note: In `liftSemilatticeInf` and `liftSemilatticeSup` below, the elaborator
+-- seems to struggle with αᵒᵈ vs α; the `by exact`s are not present in Lean 3, but without
+-- them the declarations compile much more slowly for some reason.
 -- Possibly related to the issue discussed at
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Performance.20issue.20with.20.60CompleteBooleanAlgebra.60/near/316760798
 
@@ -869,11 +870,12 @@ variable [PartialOrder α]
 @[reducible]
 def liftSemilatticeInf [SemilatticeInf β] (gi : GaloisCoinsertion l u) : SemilatticeInf α :=
   { ‹PartialOrder α› with
-    inf_le_left := fun a b =>
-      (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_left a b
-    inf_le_right := fun a b =>
-      (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_right a b
-    le_inf := fun a b c => (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).le_inf a b c
+    inf_le_left := fun a b => by
+      exact (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_left a b
+    inf_le_right := fun a b => by
+      exact (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_right a b
+    le_inf := fun a b c => by
+      exact (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).le_inf a b c
     inf := fun a b => u (l a ⊓ l b) }
 #align galois_coinsertion.lift_semilattice_inf GaloisCoinsertion.liftSemilatticeInf
 
@@ -886,11 +888,12 @@ def liftSemilatticeSup [SemilatticeSup β] (gi : GaloisCoinsertion l u) : Semila
       gi.choice (l a ⊔ l b) <|
         sup_le (gi.gc.monotone_l <| gi.gc.le_u <| le_sup_left)
           (gi.gc.monotone_l <| gi.gc.le_u <| le_sup_right)
-    le_sup_left := fun a b =>
-      (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_left a b
-    le_sup_right := fun a b =>
-      (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_right a b
-    sup_le := fun a b c => (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).sup_le a b c }
+    le_sup_left := fun a b => by
+      exact (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_left a b
+    le_sup_right := fun a b => by
+      exact (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_right a b
+    sup_le := fun a b c => by
+      exact (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).sup_le a b c }
 #align galois_coinsertion.lift_semilattice_sup GaloisCoinsertion.liftSemilatticeSup
 
 -- See note [reducible non instances]