-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : Mon (Type u)} (f : X ⟶ Y),
    Eq (α :=
      (functor ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                MonCat.carrier)).obj
          X ⟶
        Functor.obj (Mon.forget (Type u)) Y)
      ((functor ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                MonCat.carrier)).map
          f ≫
        Iso.hom
          ((fun (x : Mon (Type u)) ↦
              (Iso.refl
                  ((functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x) :
                (functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x ≅
                  (functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x))
            Y))
      (Iso.hom
          ((fun (x : Mon (Type u)) ↦
              (Iso.refl
                  ((functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x) :
                (functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x ≅
                  (functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x))
            X) ≫
        CategoryTheory.Functor.map (Mon.forget (Type u)) f)
⊢ ∀ {X Y : Mon (Type u)} (f : X ⟶ Y),
    Eq (α :=
      (functor ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                MonCat.carrier)).obj
          X ⟶
        Functor.obj (Mon.forget (Type u)) Y)
      ((functor ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                MonCat.carrier)).map
          f ≫
        Iso.hom
          ((fun (x : Mon (Type u)) ↦
              (Iso.refl
                  ((functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x) :
                (functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x ≅
                  (functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x))
            Y))
      (Iso.hom
          ((fun (x : Mon (Type u)) ↦
              (Iso.refl
                  ((functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x) :
                (functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x ≅
                  (functor ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          MonCat.carrier)).obj
                    x))
            X) ≫
        CategoryTheory.Functor.map (Mon.forget (Type u)) f)

Tactic:
cat_disch