-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
z :
  (j : J) ×
    ((F ⋙
            forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            MonCat.carrier)).obj
      j
j₁ : J
x :
  ((F ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          MonCat.carrier)).obj
    j₁
j₂ : J
y :
  ((F ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          MonCat.carrier)).obj
    j₂
obtain :
  ∀ (j₃ : J)
    (z :
      ((F ⋙
              forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              MonCat.carrier)).obj
        j₃),
    Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j₁ x) *
        (Quot.mk
            ((F ⋙
                  forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : J) ↦
              ((F ⋙
                      forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                        (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      MonCat.carrier)).obj
                j)
              j₂ y) +
          Quot.mk
            ((F ⋙
                  forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : J) ↦
              ((F ⋙
                      forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                        (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      MonCat.carrier)).obj
                j)
              j₃ z)) =
      Quot.mk
            ((F ⋙
                  forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : J) ↦
              ((F ⋙
                      forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                        (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      MonCat.carrier)).obj
                j)
              j₁ x) *
          Quot.mk
            ((F ⋙
                  forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : J) ↦
              ((F ⋙
                      forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                        (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      MonCat.carrier)).obj
                j)
              j₂ y) +
        Quot.mk
            ((F ⋙
                  forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : J) ↦
              ((F ⋙
                      forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                        (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      MonCat.carrier)).obj
                j)
              j₁ x) *
          Quot.mk
            ((F ⋙
                  forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : J) ↦
              ((F ⋙
                      forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                        (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      MonCat.carrier)).obj
                j)
              j₃ z)
⊢ Quot.mk
        ((F ⋙
              forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              MonCat.carrier)).ColimitTypeRel
        (Sigma.mk (β := fun (j : J) ↦
          ((F ⋙
                  forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier)).obj
            j)
          j₁ x) *
      (Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j₂ y) +
        Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          z) =
    Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j₁ x) *
        Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j₂ y) +
      Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j₁ x) *
        Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : 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)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          z

Tactic:
obtain ⟨j₃, z⟩ := z