-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
t : Cocone F
i : J
x : (↑(F.obj i) : Type (max u v))
j : J
y : (↑(F.obj j) : Type (max u v))
rw :
  (F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier)).descColimitType
      (((F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).coconeTypesEquiv.symm :
          (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
        (Functor.mapCocone
          (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier))
          t))
      (M.mk F
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (IsFiltered.max i j)
          (HMul.hMul (α := (↑(F.obj (IsFiltered.max i j)) : Type (max u v))) (β :=
            (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) (Y := F.obj (IsFiltered.max i j)) (F.map (IsFiltered.leftToMax i j)) :
                  (a : (↑(F.obj ⟨i, x⟩.fst) : Type (max u v))) → (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
                (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) :
              (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) (Y := F.obj (IsFiltered.max i j)) (F.map (IsFiltered.rightToMax i j)) :
                  (a : (↑(F.obj ⟨j, y⟩.fst) : Type (max u v))) → (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
                (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)) :
              (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))))) =
    HMul.hMul (α := (↑t.1 : Type (max u v))) (β := (↑t.1 : Type (max u v)))
      ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).descColimitType
          (((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).coconeTypesEquiv.symm :
              (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
            (Functor.mapCocone
              (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier))
              t))
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) :
        Functor.CoconeTypes.pt (J := J) (F :=
          F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
          (((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).coconeTypesEquiv.symm :
              (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
            (Functor.mapCocone
              (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier))
              t)))
      ((F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).descColimitType
        (((F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).coconeTypesEquiv.symm :
            (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
          (Functor.mapCocone
            (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
            t))
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)))
⊢ (F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier)).descColimitType
      (((F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).coconeTypesEquiv.symm :
          (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
        (Functor.mapCocone
          (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier))
          t))
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x) *
        M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)) =
    HMul.hMul (α := (↑t.1 : Type (max u v))) (β := (↑t.1 : Type (max u v)))
      ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).descColimitType
          (((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).coconeTypesEquiv.symm :
              (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
            (Functor.mapCocone
              (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier))
              t))
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) :
        Functor.CoconeTypes.pt (J := J) (F :=
          F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
          (((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).coconeTypesEquiv.symm :
              (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
            (Functor.mapCocone
              (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier))
              t)))
      ((F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).descColimitType
        (((F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).coconeTypesEquiv.symm :
            (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
          (Functor.mapCocone
            (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
            t))
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)))

Tactic:
rw [colimit_mul_mk_eq F ⟨i, x⟩ ⟨j, y⟩ (max' i j) (IsFiltered.leftToMax i j)
        (IsFiltered.rightToMax i j)]

Premises used: CategoryTheory.IsFiltered.rightToMax, CategoryTheory.IsFiltered.max, MonCat.FilteredColimits.colimit_mul_mk_eq, CategoryTheory.IsFiltered.leftToMax, Sigma.mk