-- 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' := ⋯ }
⊢ f ≫
      Subtype.mk (p := fun (f : Y.α →+* X.α) ↦ Continuous (X := Y.α) (Y := X.α) (⇑f : (a : Y.α) → X.α))
        (↑e_Ring.symm : Y.α →+* X.α) ⋯ =
    𝟙 X
have h : ∀ (x : X.α),
  Eq (α := X.α)
    (((↑(ConcreteCategory.hom (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α)
                (f ≫
                  Subtype.mk (p := fun (f : Y.α →+* X.α) ↦ Continuous (X := Y.α) (Y := X.α) (⇑f : (a : Y.α) → X.α))
                    (↑e_Ring.symm : Y.α →+* X.α) sorry)) :
            X.α →+* X.α) :
          (a : X.α) → X.α)
        x :
      X.α)
    (((↑(ConcreteCategory.hom (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) (𝟙 X)) :
            X.α →+* X.α) :
          (a : X.α) → X.α)
        x :
      X.α)
Tactic: ext x