-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommRingCat
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
          (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)
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
                (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)))
Tactic: ext