-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j : J
x y : (↑(F.1 j) : Type (max u v))
symm :
  HMul.hMul (α := M.{v, u} F) (β := M.{v, u} F)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Types.TypeMax.colimitCocone
                      (F ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                          (CC := carrier))).ι.app
                j) :
            (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj j)) →
              (fun (X : Type (max u v)) ↦ X)
                (((Functor.const J).obj (Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).pt).obj j))
          x :
        (fun (X : Type (max u v)) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const J)
              (Types.TypeMax.colimitCocone
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier))).pt)
            j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Types.TypeMax.colimitCocone
                      (F ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                          (CC := carrier))).ι.app
                j) :
            (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj j)) →
              (fun (X : Type (max u v)) ↦ X)
                (((Functor.const J).obj (Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).pt).obj j))
          y :
        (fun (X : Type (max u v)) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const J)
              (Types.TypeMax.colimitCocone
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier))).pt)
            j)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Types.TypeMax.colimitCocone
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier))).ι.app
            j) :
        (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj j)) →
          (fun (X : Type (max u v)) ↦ X)
            (((Functor.const J).obj (Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).pt).obj j))
      (x * y)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Types.TypeMax.colimitCocone
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier))).ι.app
            j) :
        (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj j)) →
          (fun (X : Type (max u v)) ↦ X)
            (((Functor.const J).obj (Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).pt).obj j))
      (x * y) =
    HMul.hMul (α := M.{v, u} F) (β := M.{v, u} F)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Types.TypeMax.colimitCocone
                      (F ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                          (CC := carrier))).ι.app
                j) :
            (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj j)) →
              (fun (X : Type (max u v)) ↦ X)
                (((Functor.const J).obj (Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).pt).obj j))
          x :
        (fun (X : Type (max u v)) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const J)
              (Types.TypeMax.colimitCocone
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier))).pt)
            j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Types.TypeMax.colimitCocone
                      (F ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                          (CC := carrier))).ι.app
                j) :
            (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj j)) →
              (fun (X : Type (max u v)) ↦ X)
                (((Functor.const J).obj (Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).pt).obj j))
          y :
        (fun (X : Type (max u v)) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const J)
              (Types.TypeMax.colimitCocone
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier))).pt)
            j))

Tactic:
symm