-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommMonCat
y : (↑(M.{v, u} F) : Type (max u v))
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))
obtain :
  ∀ (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))),
    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)
⊢ 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) *
      y =
    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:
obtain ⟨j, y, rfl⟩ := y.mk_surjective

Premises used: rfl, MonCat.FilteredColimits.M.mk_surjective