-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X_1 : TopCat
R : TopCommRingCat
X : TopCommRingCat
w :
  ∀ (x : TopCatᵒᵖ)
    (x_1 :
      (↑(Functor.obj
            { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
              map := fun {x x_1 : TopCatᵒᵖ} (f : x ⟶ x_1) ↦ continuousFunctions.pullback f X, map_id := ⋯,
              map_comp := ⋯ }
            x) :
        Type u)),
    Eq (α :=
      (↑(Functor.obj
            { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
              map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
              map_comp := ⋯ }
            x) :
        Type u))
      ((CommRingCat.Hom.hom
              (NatTrans.app { app := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions.map X_2 (𝟙 X), naturality := ⋯ } x) :
            (a :
                (↑({ obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                          map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                          map_comp := ⋯ }.obj
                      x) :
                  Type u)) →
              (↑({ obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                        map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                        map_comp := ⋯ }.obj
                    x) :
                Type u))
          x_1 :
        (↑(Functor.obj
              { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                map_comp := ⋯ }
              x) :
          Type u))
      ((CommRingCat.Hom.hom
              (NatTrans.app
                (𝟙
                  { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                    map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                    map_comp := ⋯ })
                x) :
            (a :
                (↑({ obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                          map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                          map_comp := ⋯ }.obj
                      x) :
                  Type u)) →
              (↑({ obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                        map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                        map_comp := ⋯ }.obj
                    x) :
                Type u))
          x_1 :
        (↑(Functor.obj
              { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                map_comp := ⋯ }
              x) :
          Type u))
⊢ Eq.{u + 2} (α :=
    Quiver.Hom (V := TopCatᵒᵖ ⥤ CommRingCat)
      { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
        map := fun {x x_1 : TopCatᵒᵖ} (f : x ⟶ x_1) ↦ continuousFunctions.pullback f X, map_id := ⋯, map_comp := ⋯ }
      { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
        map := fun {x x_1 : TopCatᵒᵖ} (f : x ⟶ x_1) ↦ continuousFunctions.pullback f X, map_id := ⋯, map_comp := ⋯ })
    { app := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions.map X_2 (𝟙 X), naturality := ⋯ }
    (𝟙
      { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
        map := fun {x x_1 : TopCatᵒᵖ} (f : x ⟶ x_1) ↦ continuousFunctions.pullback f X, map_id := ⋯, map_comp := ⋯ })

Tactic:
ext