[GOAL]
X : TopCat
T : ↑X → Type v
U : (Opens ↑X)ᵒᵖ
⊢ { obj := fun U => (x : { x // x ∈ U.unop }) → T ↑x,
          map := fun {U V} i g x => g ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x) }.map
      (𝟙 U) =
    𝟙
      ({ obj := fun U => (x : { x // x ∈ U.unop }) → T ↑x,
            map := fun {U V} i g x => g ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x) }.obj
        U)
[PROOFSTEP]
ext g
[GOAL]
case h
X : TopCat
T : ↑X → Type v
U : (Opens ↑X)ᵒᵖ
g :
  { obj := fun U => (x : { x // x ∈ U.unop }) → T ↑x,
        map := fun {U V} i g x => g ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x) }.obj
    U
⊢ { obj := fun U => (x : { x // x ∈ U.unop }) → T ↑x,
          map := fun {U V} i g x => g ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x) }.map
      (𝟙 U) g =
    𝟙
      ({ obj := fun U => (x : { x // x ∈ U.unop }) → T ↑x,
            map := fun {U V} i g x => g ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x) }.obj
        U)
      g
[PROOFSTEP]
rfl
[GOAL]
X : TopCat
T : Type v
U : (Opens ↑X)ᵒᵖ
⊢ { obj := fun U => { x // x ∈ U.unop } → T,
          map := fun {U V} i g => g ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) } }.map
      (𝟙 U) =
    𝟙
      ({ obj := fun U => { x // x ∈ U.unop } → T,
            map := fun {U V} i g => g ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) } }.obj
        U)
[PROOFSTEP]
ext g
[GOAL]
case h
X : TopCat
T : Type v
U : (Opens ↑X)ᵒᵖ
g :
  { obj := fun U => { x // x ∈ U.unop } → T,
        map := fun {U V} i g => g ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) } }.obj
    U
⊢ { obj := fun U => { x // x ∈ U.unop } → T,
          map := fun {U V} i g => g ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) } }.map
      (𝟙 U) g =
    𝟙
      ({ obj := fun U => { x // x ∈ U.unop } → T,
            map := fun {U V} i g => g ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) } }.obj
        U)
      g
[PROOFSTEP]
rfl
[GOAL]
X✝ : TopCat
X : TopCatᵒᵖ
R : TopCommRingCat
⊢ CommRing C(↑X.unop, ↑((forget₂ TopCommRingCat TopCat).obj R))
[PROOFSTEP]
infer_instance
[GOAL]
X✝ : TopCat
X Y : TopCatᵒᵖ
f : X ⟶ Y
R : TopCommRingCat
⊢ ∀ (x y : ↑(continuousFunctions X R)),
    OneHom.toFun { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
        (x * y) =
      OneHom.toFun { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
          x *
        OneHom.toFun
          { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) } y
[PROOFSTEP]
aesop_cat
[GOAL]
X✝ : TopCat
X Y : TopCatᵒᵖ
f : X ⟶ Y
R : TopCommRingCat
⊢ ∀ (x y : ↑(continuousFunctions X R)),
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(continuousFunctions X R)),
                  OneHom.toFun
                      { toFun := fun g => f.unop ≫ g,
                        map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun g => f.unop ≫ g,
                          map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun g => f.unop ≫ g,
                          map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                        y) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑(continuousFunctions X R)),
                    OneHom.toFun
                        { toFun := fun g => f.unop ≫ g,
                          map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := fun g => f.unop ≫ g,
                            map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                          x *
                        OneHom.toFun
                          { toFun := fun g => f.unop ≫ g,
                            map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑(continuousFunctions X R)),
                    OneHom.toFun
                        { toFun := fun g => f.unop ≫ g,
                          map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := fun g => f.unop ≫ g,
                            map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                          x *
                        OneHom.toFun
                          { toFun := fun g => f.unop ≫ g,
                            map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                          y) })
          y
[PROOFSTEP]
aesop_cat
[GOAL]
X✝ : TopCat
R : TopCommRingCat
X : TopCatᵒᵖ
⊢ { obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R }.map (𝟙 X) =
    𝟙 ({ obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R }.obj X)
[PROOFSTEP]
ext
[GOAL]
case w
X✝ : TopCat
R : TopCommRingCat
X : TopCatᵒᵖ
x✝ :
  (forget CommRingCat).obj
    ({ obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R }.obj X)
⊢ ↑({ obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R }.map (𝟙 X)) x✝ =
    ↑(𝟙 ({ obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R }.obj X)) x✝
[PROOFSTEP]
rfl
[GOAL]
X✝ : TopCat
X : TopCommRingCat
⊢ {
          obj := fun R =>
            CategoryTheory.Functor.mk
              { obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R },
          map := fun {R S} φ => NatTrans.mk fun X => continuousFunctions.map X φ }.map
      (𝟙 X) =
    𝟙
      ({
            obj := fun R =>
              CategoryTheory.Functor.mk
                { obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R },
            map := fun {R S} φ => NatTrans.mk fun X => continuousFunctions.map X φ }.obj
        X)
[PROOFSTEP]
ext
[GOAL]
case w.h.w
X✝ : TopCat
X : TopCommRingCat
x✝¹ : TopCatᵒᵖ
x✝ :
  (forget CommRingCat).obj
    (({
              obj := fun R =>
                CategoryTheory.Functor.mk
                  { obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R },
              map := fun {R S} φ => NatTrans.mk fun X => continuousFunctions.map X φ }.obj
          X).obj
      x✝¹)
⊢ ↑(NatTrans.app
          ({
                obj := fun R =>
                  CategoryTheory.Functor.mk
                    { obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R },
                map := fun {R S} φ => NatTrans.mk fun X => continuousFunctions.map X φ }.map
            (𝟙 X))
          x✝¹)
      x✝ =
    ↑(NatTrans.app
          (𝟙
            ({
                  obj := fun R =>
                    CategoryTheory.Functor.mk
                      { obj := fun X => continuousFunctions X R,
                        map := fun {X Y} f => continuousFunctions.pullback f R },
                  map := fun {R S} φ => NatTrans.mk fun X => continuousFunctions.map X φ }.obj
              X))
          x✝¹)
      x✝
[PROOFSTEP]
rfl
