-- 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
t : Cocone F
i : J
x : (↑(F.obj i) : Type (max u v))
j : J
y : (↑(F.obj j) : 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) *
        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)))
have 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)))
Tactic: rw [colimit_mul_mk_eq F ⟨i, x⟩ ⟨j, y⟩ (max' i j) (IsFiltered.leftToMax i j)
        (IsFiltered.rightToMax i j)]