-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X_1 : TopCat
R_1 : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
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))
⊢ 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

Tactic:
ext