-- 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
x x_1 : J
f : x ⟶ x_1
⊢ 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)
have 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' := sorry, map_add' := sorry })) :
          (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' := sorry, map_add' := sorry }) ≫
              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)))
Tactic: ext