-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered 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
⊢ MonCat.FilteredColimits.M.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))
      (Sigma.mk (β := fun (j : J) ↦
        (↑(Functor.obj
              (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))
              j) :
          Type (max u v)))
        j
        (HMul.hMul (α :=
          (↑(Functor.obj
                (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))
                j) :
            Type (max u v)))
          (β :=
          (↑(Functor.obj
                (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))
                j) :
            Type (max u v)))
          ((@ConcreteCategory.hom _ MonCat.instCategory
                  (fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) MonCat.carrier
                  (fun (X Y : MonCat) ↦
                    (MonoidHom.instFunLike :
                      FunLike ((↑X : Type (max u v)) →* (↑Y : Type (max u v))) (↑X : Type (max u v))
                        (↑Y : Type (max u v))))
                  _ _ _
                  (CategoryTheory.Functor.map
                      (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))
                      (𝟙 j) :
                    Functor.obj
                        (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))
                        (Sigma.fst (β := fun (j : J) ↦
                          (↑(Functor.obj
                                (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))
                                j) :
                            Type (max u v)))
                          (Sigma.mk (β := fun (j : J) ↦
                            (↑(Functor.obj
                                  (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))
                                  j) :
                              Type (max u v)))
                            j 0)) ⟶
                      Functor.obj
                        (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))
                        j) :
                (a : (↑((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, 0⟩.fst) : Type (max u v))) →
                  (↑((F ⋙ forget₂ SemiRingCat MonCat).obj j) : Type (max u v)))
              (Sigma.snd (β := fun (j : J) ↦
                (↑(Functor.obj
                      (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))
                      j) :
                  Type (max u v)))
                (Sigma.mk (β := fun (j : J) ↦
                  (↑(Functor.obj
                        (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))
                        j) :
                    Type (max u v)))
                  j 0)) :
            (↑(Functor.obj
                  (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))
                  j) :
              Type (max u v)))
          ((@ConcreteCategory.hom _ MonCat.instCategory
                  (fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) MonCat.carrier
                  (fun (X Y : MonCat) ↦
                    (MonoidHom.instFunLike :
                      FunLike ((↑X : Type (max u v)) →* (↑Y : Type (max u v))) (↑X : Type (max u v))
                        (↑Y : Type (max u v))))
                  _ _ _
                  (CategoryTheory.Functor.map
                      (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))
                      (𝟙 j) :
                    Functor.obj
                        (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))
                        ((Sigma.mk (β := fun (j : J) ↦
                              (↑(Functor.obj
                                    (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))
                                    j) :
                                Type (max u v)))
                              j x).fst
                          (β := fun (j : J) ↦
                          (↑(Functor.obj
                                (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))
                                j) :
                            Type (max u v)))) ⟶
                      Functor.obj
                        (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))
                        j) :
                (a : (↑((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, x⟩.fst) : Type (max u v))) →
                  (↑((F ⋙ forget₂ SemiRingCat MonCat).obj j) : Type (max u v)))
              ((Sigma.mk (β := fun (j : J) ↦
                    (↑(Functor.obj
                          (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))
                          j) :
                      Type (max u v)))
                    j x).snd
                (β := fun (j : J) ↦
                (↑(Functor.obj
                      (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))
                      j) :
                  Type (max u v)))) :
            (↑(Functor.obj
                  (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))
                  j) :
              Type (max u v))))) =
    AddMonCat.FilteredColimits.M.mk
      ((F ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat) ↦
            (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommMonCat.carrier)) ⋙
        forget₂ AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
          (CC := AddCommMonCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
          (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier))
      (Sigma.mk (β := fun (j : J) ↦
        (↑(Functor.obj
              ((F ⋙
                  forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                    (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat) ↦
                    (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommMonCat.carrier)) ⋙
                forget₂ AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat) ↦
                  (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC := AddCommMonCat.carrier) AddMonCat (FD :=
                  fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier))
              j) :
          Type (max u v)))
        j 0)
have rw : MonCat.FilteredColimits.M.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))
    (Sigma.mk (β := fun (j : J) ↦
      (↑(Functor.obj
            (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))
            j) :
        Type (max u v)))
      j
      (HMul.hMul (α :=
        (↑(Functor.obj
              (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))
              j) :
          Type (max u v)))
        (β :=
        (↑(Functor.obj
              (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))
              j) :
          Type (max u v)))
        ((@ConcreteCategory.hom _ MonCat.instCategory
                (fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) MonCat.carrier
                (fun (X Y : MonCat) ↦
                  (MonoidHom.instFunLike :
                    FunLike ((↑X : Type (max u v)) →* (↑Y : Type (max u v))) (↑X : Type (max u v))
                      (↑Y : Type (max u v))))
                _ _ _
                (𝟙
                    (Functor.obj
                      (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))
                      (Sigma.fst (β := fun (j : J) ↦
                        (↑(Functor.obj
                              (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))
                              j) :
                          Type (max u v)))
                        (Sigma.mk (β := fun (j : J) ↦
                          (↑(Functor.obj
                                (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))
                                j) :
                            Type (max u v)))
                          j 0))) :
                  Functor.obj
                      (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))
                      (Sigma.fst (β := fun (j : J) ↦
                        (↑(Functor.obj
                              (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))
                              j) :
                          Type (max u v)))
                        (Sigma.mk (β := fun (j : J) ↦
                          (↑(Functor.obj
                                (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))
                                j) :
                            Type (max u v)))
                          j 0)) ⟶
                    Functor.obj
                      (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))
                      (Sigma.fst (β := fun (j : J) ↦
                        (↑(Functor.obj
                              (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))
                              j) :
                          Type (max u v)))
                        (Sigma.mk (β := fun (j : J) ↦
                          (↑(Functor.obj
                                (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))
                                j) :
                            Type (max u v)))
                          j 0))) :
              (a : (↑((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, 0⟩.fst) : Type (max u v))) →
                (↑((F ⋙ forget₂ SemiRingCat MonCat).obj j) : Type (max u v)))
            (Sigma.snd (β := fun (j : J) ↦
              (↑(Functor.obj
                    (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))
                    j) :
                Type (max u v)))
              (Sigma.mk (β := fun (j : J) ↦
                (↑(Functor.obj
                      (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))
                      j) :
                  Type (max u v)))
                j 0)) :
          (↑(Functor.obj
                (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))
                j) :
            Type (max u v)))
        ((@ConcreteCategory.hom _ MonCat.instCategory
                (fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) MonCat.carrier
                (fun (X Y : MonCat) ↦
                  (MonoidHom.instFunLike :
                    FunLike ((↑X : Type (max u v)) →* (↑Y : Type (max u v))) (↑X : Type (max u v))
                      (↑Y : Type (max u v))))
                _ _ _
                (𝟙
                    (Functor.obj
                      (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))
                      (Sigma.fst (β := fun (j : J) ↦
                        (↑(Functor.obj
                              (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))
                              j) :
                          Type (max u v)))
                        (Sigma.mk (β := fun (j : J) ↦
                          (↑(Functor.obj
                                (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))
                                j) :
                            Type (max u v)))
                          j 0))) :
                  Functor.obj
                      (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))
                      (Sigma.fst (β := fun (j : J) ↦
                        (↑(Functor.obj
                              (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))
                              j) :
                          Type (max u v)))
                        (Sigma.mk (β := fun (j : J) ↦
                          (↑(Functor.obj
                                (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))
                                j) :
                            Type (max u v)))
                          j 0)) ⟶
                    Functor.obj
                      (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))
                      (Sigma.fst (β := fun (j : J) ↦
                        (↑(Functor.obj
                              (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))
                              j) :
                          Type (max u v)))
                        (Sigma.mk (β := fun (j : J) ↦
                          (↑(Functor.obj
                                (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))
                                j) :
                            Type (max u v)))
                          j 0))) :
              (a : (↑((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, x⟩.fst) : Type (max u v))) →
                (↑((F ⋙ forget₂ SemiRingCat MonCat).obj j) : Type (max u v)))
            ((Sigma.mk (β := fun (j : J) ↦
                  (↑(Functor.obj
                        (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))
                        j) :
                    Type (max u v)))
                  j x).snd
              (β := fun (j : J) ↦
              (↑(Functor.obj
                    (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))
                    j) :
                Type (max u v)))) :
          (↑(Functor.obj
                (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))
                j) :
            Type (max u v))))) =
  AddMonCat.FilteredColimits.M.mk
    ((F ⋙
        forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
          (CD := AddCommMonCat.carrier)) ⋙
      forget₂ AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
        (CC := AddCommMonCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
        (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier))
    (Sigma.mk (β := fun (j : J) ↦
      (↑(Functor.obj
            ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat) ↦
                  (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommMonCat.carrier)) ⋙
              forget₂ AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat) ↦
                (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC := AddCommMonCat.carrier) AddMonCat (FD :=
                fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier))
            j) :
        Type (max u v)))
      j 0)
Tactic: rw [CategoryTheory.Functor.map_id]