chore(Order): make CompleteDistribLattice.MinimalAxioms.of semireducible (#37478)

This is part of the greater discussion about whether we should make all `def`s appearing in instances `implicit_reducible`. I believe the answer in this case is pretty clearly yes sinced the sole purpose of `CompleteLattice.MinimalAxioms` is to build instances.

From APAP

Author: YaelDillies

Mathlib/Order/CompleteBooleanAlgebra.lean

@@ -224,6 +224,7 @@ variable (minAx : MinimalAxioms α)
 
 /-- The `CompleteDistribLattice.MinimalAxioms` element corresponding to a complete distrib lattice.
 -/
+@[implicit_reducible]
 def of [CompleteDistribLattice α] : MinimalAxioms α where
   __ := ‹CompleteDistribLattice α›
   inf_sSup_le_iSup_inf a s := inf_sSup_eq.le
@@ -308,6 +309,7 @@ abbrev toCompleteDistribLattice : CompleteDistribLattice.MinimalAxioms α where
       _ = _ := by simp [sInf_eq_iInf', iInf_unique, iSup_bool_eq]
 
 /-- The `CompletelyDistribLattice.MinimalAxioms` element corresponding to a frame. -/
+@[implicit_reducible]
 def of [CompletelyDistribLattice α] : MinimalAxioms α := { ‹CompletelyDistribLattice α› with }
 
 end MinimalAxioms