-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
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₁
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₂
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₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
g : j₂ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.secondToMax₃ j₁ j₂ j₃
h : j₃ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.thirdToMax₃ j₁ j₂ 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)))
        k
        (HMul.hMul (α := (↑(F.obj (IsFiltered.max₃ j₁ j₂ j₃)) : Type (max u v))) (β :=
            (↑(F.obj (IsFiltered.max₃ j₁ j₂ j₃)) : Type (max u v)))
            ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                    (CC := carrier) (F.map f) :
                  (a : (↑(F.obj j₁) : Type (max u v))) → (↑(F.obj (IsFiltered.max₃ j₁ j₂ j₃)) : Type (max u v)))
                x :
              (↑(F.obj (IsFiltered.max₃ j₁ j₂ j₃)) : Type (max u v)))
            ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                    (CC := carrier) (F.map g) :
                  (a : (↑(F.obj j₂) : Type (max u v))) → (↑(F.obj (IsFiltered.max₃ j₁ j₂ j₃)) : Type (max u v)))
                y :
              (↑(F.obj (IsFiltered.max₃ j₁ j₂ j₃)) : Type (max u v))) +
          HMul.hMul (α := (↑(F.obj (IsFiltered.max₃ j₁ j₂ j₃)) : Type (max u v))) (β :=
            (↑(F.obj (IsFiltered.max₃ j₁ j₂ j₃)) : Type (max u v)))
            ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                    (CC := carrier) (F.map f) :
                  (a : (↑(F.obj j₁) : Type (max u v))) → (↑(F.obj (IsFiltered.max₃ j₁ j₂ j₃)) : Type (max u v)))
                x :
              (↑(F.obj (IsFiltered.max₃ j₁ j₂ j₃)) : Type (max u v)))
            ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                    (CC := carrier) (F.map h) :
                  (a : (↑(F.obj j₃) : Type (max u v))) → (↑(F.obj (IsFiltered.max₃ j₁ j₂ j₃)) : Type (max u v)))
                z :
              (↑(F.obj (IsFiltered.max₃ j₁ j₂ 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)))
        k
        (HAdd.hAdd (α :=
          (↑(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))
                k) :
            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) 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))
                k) :
            Type (max u v)))
          ((@ConcreteCategory.hom _ AddMonCat.instCategory
                  (fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) AddMonCat.carrier
                  (fun (X Y : AddMonCat) ↦
                    (AddMonoidHom.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) 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))
                        k) :
                    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))
                        k ⟶
                      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))
                        k) :
                (a :
                    (↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj k) :
                      Type (max u v))) →
                  (↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj k) :
                    Type (max u v)))
              (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))
                      k) :
                  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))
                      k) :
                  Type (max u v)))
                ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                        (CC := MonCat.carrier) (X :=
                        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₁)
                        (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))
                          f) :
                      (a : (↑((F ⋙ forget₂ SemiRingCat MonCat).obj j₁) : Type (max u v))) →
                        (↑((F ⋙ forget₂ SemiRingCat MonCat).obj k) : Type (max u v)))
                    x :
                  (↑(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))
                        k) :
                    Type (max u v)))
                ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                        (CC := MonCat.carrier) (X :=
                        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₂)
                        (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))
                          g) :
                      (a : (↑((F ⋙ forget₂ SemiRingCat MonCat).obj j₂) : Type (max u v))) →
                        (↑((F ⋙ forget₂ SemiRingCat MonCat).obj k) : Type (max u v)))
                    y :
                  (↑(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))
                        k) :
                    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) 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))
                  k) :
              Type (max u v)))
          ((@ConcreteCategory.hom _ AddMonCat.instCategory
                  (fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) AddMonCat.carrier
                  (fun (X Y : AddMonCat) ↦
                    (AddMonoidHom.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) 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))
                        k) :
                    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))
                        k ⟶
                      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))
                        k) :
                (a :
                    (↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj k) :
                      Type (max u v))) →
                  (↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj k) :
                    Type (max u v)))
              (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))
                      k) :
                  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))
                      k) :
                  Type (max u v)))
                ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                        (CC := MonCat.carrier) (X :=
                        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₁)
                        (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))
                          f) :
                      (a : (↑((F ⋙ forget₂ SemiRingCat MonCat).obj j₁) : Type (max u v))) →
                        (↑((F ⋙ forget₂ SemiRingCat MonCat).obj k) : Type (max u v)))
                    x :
                  (↑(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))
                        k) :
                    Type (max u v)))
                ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                        (CC := MonCat.carrier) (X :=
                        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₃)
                        (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))
                          h) :
                      (a : (↑((F ⋙ forget₂ SemiRingCat MonCat).obj j₃) : Type (max u v))) →
                        (↑((F ⋙ forget₂ SemiRingCat MonCat).obj k) : Type (max u v)))
                    z :
                  (↑(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))
                        k) :
                    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) 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))
                  k) :
              Type (max u v)))))

Tactic:
rfl