-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
x x_1 : J
f : x ⟶ x_1
hf :
  ∀ (x_2 : (↑(F.obj x) : Type (max u v))),
    Eq (α := (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))
      ((Hom.hom
              (F.map f ≫
                ofHom
                  (let __src :=
                    MonCat.Hom.hom
                      ((MonCat.FilteredColimits.colimitCocone.{v, u}
                              (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))).ι.app
                        x_1);
                  let __src_1 :=
                    AddCommMonCat.Hom.hom
                      ((AddCommMonCat.FilteredColimits.colimitCocone.{v, u}
                              (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))).ι.app
                        x_1);
                  { toMonoidHom := __src, map_zero' := ⋯, map_add' := ⋯ })) :
            (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
          x_2 :
        (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))
      ((Hom.hom
              (ofHom
                  (let __src :=
                    MonCat.Hom.hom
                      ((MonCat.FilteredColimits.colimitCocone.{v, u}
                              (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))).ι.app
                        x);
                  let __src_1 :=
                    AddCommMonCat.Hom.hom
                      ((AddCommMonCat.FilteredColimits.colimitCocone.{v, u}
                              (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))).ι.app
                        x);
                  { toMonoidHom := __src, map_zero' := ⋯, map_add' := ⋯ }) ≫
                CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimit.{v, u} F)) f) :
            (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
          x_2 :
        (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))
⊢ Eq (α := F.obj x ⟶ Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1)
    (F.map f ≫
        ofHom
          (let __src :=
            MonCat.Hom.hom
              ((MonCat.FilteredColimits.colimitCocone.{v, u}
                      (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))).ι.app
                x_1);
          let __src_1 :=
            AddCommMonCat.Hom.hom
              ((AddCommMonCat.FilteredColimits.colimitCocone.{v, u}
                      (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))).ι.app
                x_1);
          { toMonoidHom := __src, map_zero' := ⋯, map_add' := ⋯ }) :
      F.obj x ⟶ Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1)
    (ofHom
          (let __src :=
            MonCat.Hom.hom
              ((MonCat.FilteredColimits.colimitCocone.{v, u}
                      (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))).ι.app
                x);
          let __src_1 :=
            AddCommMonCat.Hom.hom
              ((AddCommMonCat.FilteredColimits.colimitCocone.{v, u}
                      (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))).ι.app
                x);
          { toMonoidHom := __src, map_zero' := ⋯, map_add' := ⋯ }) ≫
        CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimit.{v, u} F)) f :
      F.obj x ⟶ Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1)

Tactic:
ext