Complex conditions in theorems/instances?

Stream: lean4

[Victor Porton]

I have the following theorem and also several related theorems:

noncomputable def theorem515_completeLattice
    [Filtrator.Primary α]
    [SemilatticeInf (Filtrator.subset (α := α))]
    [OrderTop α]
    [OrderBot α]
    (hcoreord :
      ∀ a b : Filtrator.subset (α := α),
        a.1 ≤ b.1 ↔
          @LE.le (Filtrator.subset (α := α))
            (inferInstance : SemilatticeInf (Filtrator.subset (α := α))).toPartialOrder.toLE
              a b) :
    CompleteLattice (Filtrator.supset (α := α)) := by
  letI : CompleteSemilatticeSup (Filtrator.supset (α := α)) :=
    theorem515_completeSemilatticeSup (α := α) hcoreord
  exact completeLatticeOfCompleteSemilatticeSup (Filtrator.supset (α := α))

You see that it has a rather complex condition hcoreord stating that the orders on "primary filtrator" and on the SemilatticeInf is the same order. How not to spell this long condition every time, when I define or use one of my theorems with such a condition? Should I turn hcoreord into a class and should I make theorem515_completeLattice an instance?

[Victor Porton]

Note that a Filtrator.Primary a class derived from PartialOrder.