-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommRingCat
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
                  (RingCat.Hom.hom
                    ((RingCat.FilteredColimits.colimitCocone.{v, u}
                            (F ⋙
                              forget₂ CommRingCat (FC := fun (R S : CommRingCat) ↦
                                (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) RingCat (FD :=
                                fun (R S : RingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CD :=
                                RingCat.carrier))).ι.app
                      x_1))) :
            (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
                  (RingCat.Hom.hom
                    ((RingCat.FilteredColimits.colimitCocone.{v, u}
                            (F ⋙
                              forget₂ CommRingCat (FC := fun (R S : CommRingCat) ↦
                                (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) RingCat (FD :=
                                fun (R S : RingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CD :=
                                RingCat.carrier))).ι.app
                      x)) ≫
                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
          (RingCat.Hom.hom
            ((RingCat.FilteredColimits.colimitCocone.{v, u}
                    (F ⋙
                      forget₂ CommRingCat (FC := fun (R S : CommRingCat) ↦
                        (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) RingCat (FD :=
                        fun (R S : RingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CD :=
                        RingCat.carrier))).ι.app
              x_1)) :
      F.obj x ⟶ Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1)
    (ofHom
          (RingCat.Hom.hom
            ((RingCat.FilteredColimits.colimitCocone.{v, u}
                    (F ⋙
                      forget₂ CommRingCat (FC := fun (R S : CommRingCat) ↦
                        (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) RingCat (FD :=
                        fun (R S : RingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CD :=
                        RingCat.carrier))).ι.app
              x)) ≫
        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