by exact

Stream: mathlib4

[Kevin Buzzard]

These two declarations elaborate far more slowly in mathlib4 than mathlib3. I tried the experiment of making OrderDual a one-field structure and then discovered that actually some of the proofs naturally elaborate to be proofs about αᵒᵈᵒᵈ rather than α. For example in line 876 we see le_inf := fun a b c => (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).le_inf a b c but OrderDual.semilatticeInf (α : Type u_1) [SemilatticeSup α] : SemilatticeInf αᵒᵈ. The refactor made me have to struggle more to get these proofs to typecheck.

At some point I hit on adding by exact to these proofs, and it magically makes all the timeouts go away, whether or not OrderDual is a one field structure. For example in place of the lines quoted above we do this:

@[reducible]
def liftSemilatticeInf [SemilatticeInf β] (gi : GaloisCoinsertion l u) : SemilatticeInf α :=
  { ‹PartialOrder α› with
    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

-- See note [reducible non instances]
/-- Lift the suprema along a Galois coinsertion -/
@[reducible]
def liftSemilatticeSup [SemilatticeSup β] (gi : GaloisCoinsertion l u) : SemilatticeSup α :=
  { ‹PartialOrder α› with
    sup := fun a b => 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 =>
      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

then these declarations elaborate instantly, rather than taking a couple of seconds on this machine. Why might this be?