Commit 2025-06-04 18:15 ac1246f8

feat(CategoryTheory/Monoidal): define Mon_ by using Mon_Class (#24646) The main change is from

structure Mon_ where
  X : C
  one : 𝟙_ C ⟶ X
  mul : X ⊗ X ⟶ X
  one_mul : (one ▷ X) ≫ mul = (λ_ X).hom := by aesop_cat
  mul_one : (X ◁ one) ≫ mul = (ρ_ X).hom := by aesop_cat
  mul_assoc : (mul ▷ X) ≫ mul = (α_ X X X).hom ≫ (X ◁ mul) ≫ mul := by aesop_cat

to

structure Mon_ where
  X : C
  [mon : Mon_Class X]

• depends on: #24597