-- Lean 4 proof step from Mathlib.Topology.Category.TopCommRingCat (goal)
Goal:
X Y : TopCommRingCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
        { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
        fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
      X)
    (CategoryTheory.Functor.map
      (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
        { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
        fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
      f)
i_Top : Functor.obj
    (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
      { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
      fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
    X ≅
  Functor.obj
    (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
      { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
      fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
        { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
        fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
      f)
e_Ring : X.α ≃+* Y.α :=
  let __src := (↑f : X.α →+* Y.α);
  let __src_1 :
    Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier))
        (Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
            fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
          X) ≃
      Functor.obj
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier))
        (Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
            fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
          Y) :=
    Iso.toEquiv
      (Functor.mapIso
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)) i_Top);
  { toFun := (↑(↑__src : X.α →* Y.α) : OneHom X.α Y.α).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯,
    map_mul' := ⋯, map_add' := ⋯ }
⊢ Subtype.mk (p := fun (f : Y.α →+* X.α) ↦ Continuous (X := Y.α) (Y := X.α) (⇑f : (a : Y.α) → X.α))
        (↑e_Ring.symm : Y.α →+* X.α) ⋯ ≫
      f =
    𝟙 Y
have h : ∀ (x : Y.α),
  Eq (α := Y.α)
    (((↑(ConcreteCategory.hom (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) (X := Y)
                (Subtype.mk (p := fun (f : Y.α →+* X.α) ↦ Continuous (X := Y.α) (Y := X.α) (⇑f : (a : Y.α) → X.α))
                    (↑e_Ring.symm : Y.α →+* X.α) sorry ≫
                  f)) :
            Y.α →+* Y.α) :
          (a : Y.α) → Y.α)
        x :
      Y.α)
    (((↑(ConcreteCategory.hom (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) (𝟙 Y)) :
            Y.α →+* Y.α) :
          (a : Y.α) → Y.α)
        x :
      Y.α)
Tactic: ext x