-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
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))
⊢ (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))
have 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)
Tactic: symm