-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X_1 : TopCat
R_1 : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x x_1 :
  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))
      R
⊢ (x * x_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))
        φ =
    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 := TopCommRingCat.α)
            TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
          φ *
      x_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))
          φ
have w : ∀ (x_2 : (↑(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 * x_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_2 :
      (↑(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 ≫
                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))
                  φ *
              x_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_2 :
      (↑(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