-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommMonCat
i : J
x :
  (↑(Functor.obj
        (F ⋙
          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier))
        i) :
    Type (max u v))
j : J
y :
  (↑(Functor.obj
        (F ⋙
          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier))
        j) :
    Type (max u v))
k : J := IsFiltered.max i j
f : i ⟶ IsFiltered.max i j := IsFiltered.leftToMax i j
g : j ⟶ IsFiltered.max i j := IsFiltered.rightToMax i j
rw :
  MonCat.FilteredColimits.M.mk
      (F ⋙
        forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
          MonCat.carrier))
      (Sigma.mk (β := fun (j : J) ↦
        (↑(Functor.obj
              (F ⋙
                forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier))
              j) :
          Type (max u v)))
        k
        (HMul.hMul (α :=
          (↑(Functor.obj
                (F ⋙
                  forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
                    (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                k) :
            Type (max u v)))
          (β :=
          (↑(Functor.obj
                (F ⋙
                  forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
                    (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                k) :
            Type (max u v)))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier) (X :=
                  Functor.obj
                    (F ⋙
                      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                        (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                        fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                    (Sigma.fst (β := fun (j : J) ↦
                      (↑(Functor.obj
                            (F ⋙
                              forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                                (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                                fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                                MonCat.carrier))
                            j) :
                        Type (max u v)))
                      (Sigma.mk (β := fun (j : J) ↦
                        (↑(Functor.obj
                              (F ⋙
                                forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                                  (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                                  fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                                  MonCat.carrier))
                              j) :
                          Type (max u v)))
                        i x)))
                  (CategoryTheory.Functor.map
                    (F ⋙
                      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                        (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                        fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                    f) :
                (a : (↑((F ⋙ forget₂ CommMonCat MonCat).obj ⟨i, x⟩.fst) : Type (max u v))) →
                  (↑((F ⋙ forget₂ CommMonCat MonCat).obj k) : Type (max u v)))
              (Sigma.snd (β := fun (j : J) ↦
                (↑(Functor.obj
                      (F ⋙
                        forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                          (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                          fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                          MonCat.carrier))
                      j) :
                  Type (max u v)))
                (Sigma.mk (β := fun (j : J) ↦
                  (↑(Functor.obj
                        (F ⋙
                          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                            (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                            fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                            MonCat.carrier))
                        j) :
                    Type (max u v)))
                  i x)) :
            (↑(Functor.obj
                  (F ⋙
                    forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                      (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                  k) :
              Type (max u v)))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier) (X :=
                  Functor.obj
                    (F ⋙
                      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                        (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                        fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                    (Sigma.fst (β := fun (j : J) ↦
                      (↑(Functor.obj
                            (F ⋙
                              forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                                (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                                fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                                MonCat.carrier))
                            j) :
                        Type (max u v)))
                      (Sigma.mk (β := fun (j : J) ↦
                        (↑(Functor.obj
                              (F ⋙
                                forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                                  (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                                  fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                                  MonCat.carrier))
                              j) :
                          Type (max u v)))
                        j y)))
                  (CategoryTheory.Functor.map
                    (F ⋙
                      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                        (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                        fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                    g) :
                (a : (↑((F ⋙ forget₂ CommMonCat MonCat).obj ⟨j, y⟩.fst) : Type (max u v))) →
                  (↑((F ⋙ forget₂ CommMonCat MonCat).obj k) : Type (max u v)))
              (Sigma.snd (β := fun (j : J) ↦
                (↑(Functor.obj
                      (F ⋙
                        forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                          (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                          fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                          MonCat.carrier))
                      j) :
                  Type (max u v)))
                (Sigma.mk (β := fun (j : J) ↦
                  (↑(Functor.obj
                        (F ⋙
                          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                            (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                            fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                            MonCat.carrier))
                        j) :
                    Type (max u v)))
                  j y)) :
            (↑(Functor.obj
                  (F ⋙
                    forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                      (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                  k) :
              Type (max u v))))) =
    MonCat.FilteredColimits.M.mk
      (F ⋙
        forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
          MonCat.carrier))
      (Sigma.mk (β := fun (j : J) ↦
        (↑(Functor.obj
              (F ⋙
                forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier))
              j) :
          Type (max u v)))
        k
        (HMul.hMul (α :=
          (↑(Functor.obj
                (F ⋙
                  forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
                    (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                k) :
            Type (max u v)))
          (β :=
          (↑(Functor.obj
                (F ⋙
                  forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
                    (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                k) :
            Type (max u v)))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier) (X :=
                  Functor.obj
                    (F ⋙
                      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                        (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                        fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                    (Sigma.fst (β := fun (j : J) ↦
                      (↑(Functor.obj
                            (F ⋙
                              forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                                (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                                fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                                MonCat.carrier))
                            j) :
                        Type (max u v)))
                      (Sigma.mk (β := fun (j : J) ↦
                        (↑(Functor.obj
                              (F ⋙
                                forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                                  (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                                  fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                                  MonCat.carrier))
                              j) :
                          Type (max u v)))
                        j y)))
                  (CategoryTheory.Functor.map
                    (F ⋙
                      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                        (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                        fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                    g) :
                (a : (↑((F ⋙ forget₂ CommMonCat MonCat).obj ⟨j, y⟩.fst) : Type (max u v))) →
                  (↑((F ⋙ forget₂ CommMonCat MonCat).obj k) : Type (max u v)))
              (Sigma.snd (β := fun (j : J) ↦
                (↑(Functor.obj
                      (F ⋙
                        forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                          (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                          fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                          MonCat.carrier))
                      j) :
                  Type (max u v)))
                (Sigma.mk (β := fun (j : J) ↦
                  (↑(Functor.obj
                        (F ⋙
                          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                            (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                            fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                            MonCat.carrier))
                        j) :
                    Type (max u v)))
                  j y)) :
            (↑(Functor.obj
                  (F ⋙
                    forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                      (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                  k) :
              Type (max u v)))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier) (X :=
                  Functor.obj
                    (F ⋙
                      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                        (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                        fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                    (Sigma.fst (β := fun (j : J) ↦
                      (↑(Functor.obj
                            (F ⋙
                              forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                                (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                                fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                                MonCat.carrier))
                            j) :
                        Type (max u v)))
                      (Sigma.mk (β := fun (j : J) ↦
                        (↑(Functor.obj
                              (F ⋙
                                forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                                  (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                                  fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                                  MonCat.carrier))
                              j) :
                          Type (max u v)))
                        i x)))
                  (CategoryTheory.Functor.map
                    (F ⋙
                      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                        (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                        fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                    f) :
                (a : (↑((F ⋙ forget₂ CommMonCat MonCat).obj ⟨i, x⟩.fst) : Type (max u v))) →
                  (↑((F ⋙ forget₂ CommMonCat MonCat).obj k) : Type (max u v)))
              (Sigma.snd (β := fun (j : J) ↦
                (↑(Functor.obj
                      (F ⋙
                        forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                          (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                          fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                          MonCat.carrier))
                      j) :
                  Type (max u v)))
                (Sigma.mk (β := fun (j : J) ↦
                  (↑(Functor.obj
                        (F ⋙
                          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                            (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                            fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
                            MonCat.carrier))
                        j) :
                    Type (max u v)))
                  i x)) :
            (↑(Functor.obj
                  (F ⋙
                    forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                      (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                  k) :
              Type (max u v)))))
⊢ MonCat.FilteredColimits.M.mk
        (F ⋙
          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier))
        (Sigma.mk (β := fun (j : J) ↦
          (↑(Functor.obj
                (F ⋙
                  forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
                    (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                j) :
            Type (max u v)))
          i x) *
      MonCat.FilteredColimits.M.mk
        (F ⋙
          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier))
        (Sigma.mk (β := fun (j : J) ↦
          (↑(Functor.obj
                (F ⋙
                  forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
                    (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                j) :
            Type (max u v)))
          j y) =
    MonCat.FilteredColimits.M.mk
        (F ⋙
          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier))
        (Sigma.mk (β := fun (j : J) ↦
          (↑(Functor.obj
                (F ⋙
                  forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
                    (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                j) :
            Type (max u v)))
          j y) *
      MonCat.FilteredColimits.M.mk
        (F ⋙
          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier))
        (Sigma.mk (β := fun (j : J) ↦
          (↑(Functor.obj
                (F ⋙
                  forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
                    (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                j) :
            Type (max u v)))
          i x)

Tactic:
rw [colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩ ⟨j, y⟩ k f g,
        colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ ⟨i, x⟩ k g f]