-- Module: Mathlib.Topology.Sheaves.CommRingCat
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
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))
⊢ (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))
          φ

Tactic:
ext