-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X_1 : TopCat
R_1 : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
⊢ Eq (α :=
    unop X ⟶
      Functor.obj
        (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
          { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
          TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
        S)
    (1 ≫
      CategoryTheory.Functor.map
        (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
          { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
          TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
        φ)
    1
have w : ∀ (x : (↑(unop X) : Type u)),
  Eq (α :=
    (↑(Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
            TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
          S) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            unop X) (Y :=
            Functor.obj
              (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
                TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
              S)
            (1 ≫
              CategoryTheory.Functor.map
                (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                  { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC :=
                  TopCommRingCat.α) TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD :=
                  carrier))
                φ) :
          (a : (↑(unop X) : Type u)) → (↑((forget₂ TopCommRingCat TopCat).obj S) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
              { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
              TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
            S) :
        Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (unop X)
            (Functor.obj
              (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
                TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
              S)
            1 :
          (a : (↑(unop X) : Type u)) → (↑((forget₂ TopCommRingCat TopCat).obj S) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
              { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
              TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
            S) :
        Type u))
Tactic: ext