-- 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
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)))

Tactic:
simpa using (Types.TypeMax.colimitCocone (F ⋙ forget SemiRingCat)).ι.naturality_apply f _

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.Limits.Types.TypeMax.colimitCocone, CategoryTheory.Functor.comp, CategoryTheory.Limits.Cocone.ι, CategoryTheory.forget, SemiRingCat