-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
this_1 :
  Functor.ReflectsIsomorphisms
    (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) RingCat
      (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier))
this_2 :
  Small.{u, max u v}
    (↑((F ⋙
              forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier)) ⋙
            forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              RingCat.carrier)).sections :
      Type (max u v))
F' : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat :=
  F ⋙
    forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) RingCat
        (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier) ⋙
      forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier)
this :
  Small.{u, max u v}
    (↑(F' ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              SemiRingCat.carrier)).sections :
      Type (max u v))
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    Functor.obj.{w, u, v, u + 1}
        (Functor.obj (Functor.const J)
          (of
            (Types.Small.limitCone
                (F ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier))).pt))
        x ⟶
      F.obj x_1)
    (CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          (of
            (Types.Small.limitCone
                (F ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier))).pt))
        f ≫
      ofHom (SemiRingCat.limitπRingHom F' x_1))
    (ofHom (SemiRingCat.limitπRingHom F' x) ≫ F.map f)
have hf : ∀
  (x_2 :
    (↑(Functor.obj.{w, u, v, u + 1}
          (Functor.obj (Functor.const J)
            (of
              (Types.Small.limitCone
                  (F ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier))).pt))
          x) :
      Type u)),
  Eq (α := (↑(F.obj x_1) : Type u))
    ((Hom.hom
            (CategoryTheory.Functor.map
                (Functor.obj (Functor.const J)
                  (of
                    (Types.Small.limitCone
                        (F ⋙
                          forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := carrier))).pt))
                f ≫
              ofHom (SemiRingCat.limitπRingHom F' x_1)) :
          (a : (↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget CommRingCat)).pt)).obj x) : Type u)) →
            (↑(F.obj x_1) : Type u))
        x_2 :
      (↑(F.obj x_1) : Type u))
    ((Hom.hom (ofHom (SemiRingCat.limitπRingHom F' x) ≫ F.map f) :
          (a : (↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget CommRingCat)).pt)).obj x) : Type u)) →
            (↑(F.obj x_1) : Type u))
        x_2 :
      (↑(F.obj x_1) : Type u))
Tactic: ext