-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J RingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)).sections :
      Type (max u v))
this_1 :
  Functor.ReflectsIsomorphisms
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := 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₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                SemiRingCat.carrier)) ⋙
            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
hf :
  ∀
    (x_2 :
      (↑(Functor.obj.{w, u, v, u + 1}
            (Functor.obj (Functor.const J)
              (of
                (Types.Small.limitCone
                    (F ⋙
                      forget RingCat (FC := fun (R S : RingCat.{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 RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                              carrier))).pt))
                  f ≫
                ofHom
                  (SemiRingCat.limitπRingHom
                    (F ⋙
                      forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                        SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                        SemiRingCat.carrier))
                    x_1)) :
            (a : (↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget RingCat)).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 ⋙
                      forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                        SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                        SemiRingCat.carrier))
                    x) ≫
                F.map f) :
            (a : (↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget RingCat)).pt)).obj x) : Type u)) →
              (↑(F.obj x_1) : Type u))
          x_2 :
        (↑(F.obj x_1) : Type u))
⊢ Eq (α :=
    Functor.obj.{w, u, v, u + 1}
        (Functor.obj (Functor.const J)
          (of
            (Types.Small.limitCone
                (F ⋙
                  forget RingCat (FC := fun (R S : RingCat.{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 RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier))).pt))
        f ≫
      ofHom
        (SemiRingCat.limitπRingHom
          (F ⋙
            forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
              SemiRingCat.carrier))
          x_1))
    (ofHom
        (SemiRingCat.limitπRingHom
          (F ⋙
            forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
              SemiRingCat.carrier))
          x) ≫
      F.map f)

Tactic:
ext