[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), NatTrans.app f (op U) = NatTrans.app g (op U)
⊢ f = g
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case app
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), NatTrans.app f (op U) = NatTrans.app g (op U)
⊢ f.app = g.app
[PROOFSTEP]
ext U
[GOAL]
case app.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), NatTrans.app f (op U) = NatTrans.app g (op U)
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app f U = NatTrans.app g U
[PROOFSTEP]
induction U with
| _ U => ?_
[GOAL]
case app.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), NatTrans.app f (op U) = NatTrans.app g (op U)
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app f U = NatTrans.app g U
[PROOFSTEP]
induction U with
| _ U => ?_
[GOAL]
case app.h.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), NatTrans.app f (op U) = NatTrans.app g (op U)
U : Opens ↑X
⊢ NatTrans.app f (op U) = NatTrans.app g (op U)
[PROOFSTEP]
apply w
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
v w x y z : Opens ↑X
h₀ : v ≤ x
h₁ : x ≤ z ⊓ w
h₂ : x ≤ y ⊓ z
⊢ v ≤ y
[PROOFSTEP]
restrict_tac
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
X : TopCat
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : ConcreteCategory C
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : (forget C).obj (F.obj (op W))
⊢ x |_ V |_ U = x |_ U
[PROOFSTEP]
delta restrictOpen restrict
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
X : TopCat
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : ConcreteCategory C
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : (forget C).obj (F.obj (op W))
⊢ ↑(F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op) (↑(F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑V → a ∈ ↑W)).op) x) =
    ↑(F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑W)).op) x
[PROOFSTEP]
rw [← comp_apply, ← Functor.map_comp]
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
X : TopCat
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : ConcreteCategory C
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : (forget C).obj (F.obj (op W))
⊢ ↑(F.map ((homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑V → a ∈ ↑W)).op ≫ (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op)) x =
    ↑(F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑W)).op) x
[PROOFSTEP]
rfl
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
X : TopCat
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : ConcreteCategory C
F G : Presheaf C X
e : F ⟶ G
U V : Opens ↑X
h : U ≤ V
x : (forget C).obj (F.obj (op V))
⊢ ↑(NatTrans.app e (op U)) (x |_ U) = ↑(NatTrans.app e (op V)) x |_ U
[PROOFSTEP]
delta restrictOpen restrict
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
X : TopCat
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : ConcreteCategory C
F G : Presheaf C X
e : F ⟶ G
U V : Opens ↑X
h : U ≤ V
x : (forget C).obj (F.obj (op V))
⊢ ↑(NatTrans.app e (op U)) (↑(F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op) x) =
    ↑(G.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op) (↑(NatTrans.app e (op V)) x)
[PROOFSTEP]
rw [← comp_apply, NatTrans.naturality, comp_apply]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
⊢ f _* ℱ = g _* ℱ
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map f).op.obj U ⟶ (Opens.map g).op.obj U
[PROOFSTEP]
dsimp [Functor.op]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ op ((Opens.map f).obj U.unop) ⟶ op ((Opens.map g).obj U.unop)
[PROOFSTEP]
apply Quiver.Hom.op
[GOAL]
case f
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map g).obj U.unop ⟶ (Opens.map f).obj U.unop
[PROOFSTEP]
apply eqToHom
[GOAL]
case f.p
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map g).obj U.unop = (Opens.map f).obj U.unop
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ NatTrans.app (pushforwardEq h ℱ).hom U =
    ℱ.map (id (eqToHom (_ : (Opens.map g).obj U.unop = (Opens.map f).obj U.unop)).op)
[PROOFSTEP]
simp [pushforwardEq]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map f).op.obj U = (Opens.map g).op.obj U
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ NatTrans.app (eqToHom (_ : f _* ℱ = g _* ℱ)) U = ℱ.map (eqToHom (_ : (Opens.map f).op.obj U = (Opens.map g).op.obj U))
[PROOFSTEP]
rw [eqToHom_app, eqToHom_map]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C X
U : Opens ↑Y
⊢ NatTrans.app (pushforwardEq (_ : f = f) ℱ).hom (op U) = 𝟙 ((f _* ℱ).obj (op U))
[PROOFSTEP]
dsimp [pushforwardEq]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C X
U : Opens ↑Y
⊢ ℱ.map (𝟙 (op ((Opens.map f).obj U))) = 𝟙 (ℱ.obj (op ((Opens.map f).obj U)))
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
⊢ 𝟙 X _* ℱ = ℱ
[PROOFSTEP]
unfold pushforwardObj
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
⊢ (Opens.map (𝟙 X)).op ⋙ ℱ = ℱ
[PROOFSTEP]
rw [Opens.map_id_eq]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
⊢ (𝟭 (Opens ↑X)).op ⋙ ℱ = ℱ
[PROOFSTEP]
erw [Functor.id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
U : Set ↑X
p : IsOpen U
⊢ NatTrans.app (id ℱ).hom (op { carrier := U, is_open' := p }) = ℱ.map (𝟙 (op { carrier := U, is_open' := p }))
[PROOFSTEP]
dsimp [id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
U : Set ↑X
p : IsOpen U
⊢ NatTrans.app (whiskerRight (NatTrans.op (Opens.mapId X).inv) ℱ ≫ (Functor.leftUnitor ℱ).hom)
      (op { carrier := U, is_open' := p }) =
    ℱ.map (𝟙 (op { carrier := U, is_open' := p }))
[PROOFSTEP]
simp [CategoryStruct.comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (id ℱ).hom U = ℱ.map (eqToHom (_ : (Opens.map (𝟙 X)).op.obj U = U))
[PROOFSTEP]
induction U
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
X✝ : Opens ↑X
⊢ NatTrans.app (id ℱ).hom (op X✝) = ℱ.map (eqToHom (_ : (Opens.map (𝟙 X)).op.obj (op X✝) = op X✝))
[PROOFSTEP]
apply id_hom_app'
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
U : Set ↑X
p : IsOpen U
⊢ NatTrans.app (id ℱ).inv (op { carrier := U, is_open' := p }) = ℱ.map (𝟙 (op { carrier := U, is_open' := p }))
[PROOFSTEP]
dsimp [id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
U : Set ↑X
p : IsOpen U
⊢ NatTrans.app ((Functor.leftUnitor ℱ).inv ≫ whiskerRight (NatTrans.op (Opens.mapId X).hom) ℱ)
      (op { carrier := U, is_open' := p }) =
    ℱ.map (𝟙 (op { carrier := U, is_open' := p }))
[PROOFSTEP]
simp [CategoryStruct.comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
U : (Opens ↑Z)ᵒᵖ
⊢ NatTrans.app (comp ℱ f g).hom U = 𝟙 (((f ≫ g) _* ℱ).obj U)
[PROOFSTEP]
simp [comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
U : (Opens ↑Z)ᵒᵖ
⊢ NatTrans.app (comp ℱ f g).inv U = 𝟙 ((g _* (f _* ℱ)).obj U)
[PROOFSTEP]
simp [comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ 𝒢 : Presheaf C X
α : ℱ ⟶ 𝒢
x✝¹ x✝ : (Opens ↑Y)ᵒᵖ
i : x✝¹ ⟶ x✝
⊢ (f _* ℱ).map i ≫ (fun U => NatTrans.app α ((Opens.map f).op.obj U)) x✝ =
    (fun U => NatTrans.app α ((Opens.map f).op.obj U)) x✝¹ ≫ (f _* 𝒢).map i
[PROOFSTEP]
erw [α.naturality]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ 𝒢 : Presheaf C X
α : ℱ ⟶ 𝒢
x✝¹ x✝ : (Opens ↑Y)ᵒᵖ
i : x✝¹ ⟶ x✝
⊢ NatTrans.app α ((Opens.map f).op.obj x✝¹) ≫ 𝒢.map ((Opens.map f).op.map i) =
    (fun U => NatTrans.app α ((Opens.map f).op.obj U)) x✝¹ ≫ (f _* 𝒢).map i
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
⊢ (pullbackObj f ℱ).obj (op U) ≅ ℱ.obj (op { carrier := ↑f '' ↑U, is_open' := H })
[PROOFSTEP]
let x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (@homOfLE _ _ _ ((Opens.map f).obj ⟨_, H⟩) (Set.image_preimage.le_u_l _)).op
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
⊢ (pullbackObj f ℱ).obj (op U) ≅ ℱ.obj (op { carrier := ↑f '' ↑U, is_open' := H })
[PROOFSTEP]
have hx : IsTerminal x :=
  { lift := fun s ↦ by
      fapply CostructuredArrow.homMk
      change op (unop _) ⟶ op (⟨_, H⟩ : Opens _)
      · refine' (homOfLE _).op
        apply (Set.image_subset f s.pt.hom.unop.le).trans
        exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)
      ·
        simp
          -- porting note : add `fac`, `uniq` manually
    fac := fun _ _ => by ext; simp
    uniq := fun _ _ _ => by ext; simp }
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ s.pt ⟶ (asEmptyCone x).pt
[PROOFSTEP]
fapply CostructuredArrow.homMk
[GOAL]
case g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ s.pt.left ⟶ (asEmptyCone x).pt.left
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ autoParam ((Opens.map f).op.map ?g ≫ (asEmptyCone x).pt.hom = s.pt.hom) _auto✝
[PROOFSTEP]
change op (unop _) ⟶ op (⟨_, H⟩ : Opens _)
[GOAL]
case g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ op s.pt.1.unop ⟶ op { carrier := ↑f '' ↑U, is_open' := H }
[PROOFSTEP]
refine' (homOfLE _).op
[GOAL]
case g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ { carrier := ↑f '' ↑U, is_open' := H } ≤ s.pt.1.unop
[PROOFSTEP]
apply (Set.image_subset f s.pt.hom.unop.le).trans
[GOAL]
case g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ ↑f '' ↑((Opens.map f).op.obj s.pt.left).unop ⊆ ↑s.pt.1.unop
[PROOFSTEP]
exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ autoParam
    ((Opens.map f).op.map
          (let_fun this := (homOfLE (_ : ↑f '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
          this) ≫
        (asEmptyCone x).pt.hom =
      s.pt.hom)
    _auto✝
[PROOFSTEP]
simp
  -- porting note : add `fac`, `uniq` manually
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
x✝¹ : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
x✝ : Discrete PEmpty
⊢ (fun s =>
          CostructuredArrow.homMk
            (let_fun this := (homOfLE (_ : ↑f '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
            this))
        x✝¹ ≫
      NatTrans.app (asEmptyCone x).π x✝ =
    NatTrans.app x✝¹.π x✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
x✝¹ : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
x✝ : Discrete PEmpty
⊢ ((fun s =>
            CostructuredArrow.homMk
              (let_fun this :=
                (homOfLE (_ : ↑f '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
              this))
          x✝¹ ≫
        NatTrans.app (asEmptyCone x).π x✝).left =
    (NatTrans.app x✝¹.π x✝).left
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
x✝² : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
x✝¹ : x✝².pt ⟶ (asEmptyCone x).pt
x✝ : ∀ (j : Discrete PEmpty), x✝¹ ≫ NatTrans.app (asEmptyCone x).π j = NatTrans.app x✝².π j
⊢ x✝¹ =
    (fun s =>
        CostructuredArrow.homMk
          (let_fun this := (homOfLE (_ : ↑f '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
          this))
      x✝²
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
x✝² : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
x✝¹ : x✝².pt ⟶ (asEmptyCone x).pt
x✝ : ∀ (j : Discrete PEmpty), x✝¹ ≫ NatTrans.app (asEmptyCone x).π j = NatTrans.app x✝².π j
⊢ x✝¹.left =
    ((fun s =>
          CostructuredArrow.homMk
            (let_fun this := (homOfLE (_ : ↑f '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
            this))
        x✝²).left
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
hx : IsTerminal x
⊢ (pullbackObj f ℱ).obj (op U) ≅ ℱ.obj (op { carrier := ↑f '' ↑U, is_open' := H })
[PROOFSTEP]
exact IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (colimitOfDiagramTerminal hx _)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : (Opens ↑Y)ᵒᵖ
⊢ IsOpen (↑(𝟙 Y) '' ↑U.unop)
[PROOFSTEP]
simpa using U.unop.2
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : (Opens ↑Y)ᵒᵖ
⊢ op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
⊢ (pullbackObj (𝟙 Y) ℱ).map i ≫
      ((fun U =>
            pullbackObjObjOfImageOpen (𝟙 Y) ℱ U.unop (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) ≪≫
              ℱ.mapIso
                (eqToIso (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U)))
          V).hom =
    ((fun U =>
            pullbackObjObjOfImageOpen (𝟙 Y) ℱ U.unop (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) ≪≫
              ℱ.mapIso
                (eqToIso (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U)))
          U).hom ≫
      ℱ.map i
[PROOFSTEP]
simp only [pullbackObj_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
⊢ (pullbackObj (𝟙 Y) ℱ).map i ≫
      (pullbackObjObjOfImageOpen (𝟙 Y) ℱ V.unop (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) ≪≫
          ℱ.mapIso
            (eqToIso (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V))).hom =
    (pullbackObjObjOfImageOpen (𝟙 Y) ℱ U.unop (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) ≪≫
          ℱ.mapIso
            (eqToIso (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U))).hom ≫
      ℱ.map i
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
j✝ : CostructuredArrow (Opens.map (𝟙 Y)).op U
⊢ colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ U) j✝ ≫
      (pullbackObj (𝟙 Y) ℱ).map i ≫
        (pullbackObjObjOfImageOpen (𝟙 Y) ℱ V.unop (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) ≪≫
            ℱ.mapIso
              (eqToIso
                (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V))).hom =
    colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ U) j✝ ≫
      (pullbackObjObjOfImageOpen (𝟙 Y) ℱ U.unop (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) ≪≫
            ℱ.mapIso
              (eqToIso
                (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U))).hom ≫
        ℱ.map i
[PROOFSTEP]
simp only [Functor.comp_obj, CostructuredArrow.proj_obj, pullbackObj_map, Iso.trans_hom, Functor.mapIso_hom,
  eqToIso.hom, Category.assoc]
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
j✝ : CostructuredArrow (Opens.map (𝟙 Y)).op U
⊢ colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ U) j✝ ≫
      colimit.pre (Lan.diagram (Opens.map (𝟙 Y)).op ℱ V) (CostructuredArrow.map i) ≫
        (pullbackObjObjOfImageOpen (𝟙 Y) ℱ V.unop (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop))).hom ≫
          ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V)) =
    colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ U) j✝ ≫
      (pullbackObjObjOfImageOpen (𝟙 Y) ℱ U.unop (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop))).hom ≫
        ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U)) ≫
          ℱ.map i
[PROOFSTEP]
erw [colimit.pre_desc_assoc, colimit.ι_desc_assoc, colimit.ι_desc_assoc]
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
j✝ : CostructuredArrow (Opens.map (𝟙 Y)).op U
⊢ NatTrans.app
        (Cocone.whisker (CostructuredArrow.map i)
            (coconeOfDiagramTerminal
              (IsLimit.mk fun s =>
                CostructuredArrow.homMk
                  (let_fun this :=
                    (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op V.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
                  this))
              (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op V.unop)))).ι
        j✝ ≫
      ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V)) =
    NatTrans.app
        (coconeOfDiagramTerminal
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (let_fun this :=
                  (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
                this))
            (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U.unop))).ι
        j✝ ≫
      ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U)) ≫
        ℱ.map i
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
j✝ : CostructuredArrow (Opens.map (𝟙 Y)).op U
⊢ ℱ.map
        (IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op V.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            ((CostructuredArrow.map i).obj j✝)).left ≫
      ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V)) =
    ℱ.map
        (IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            j✝).left ≫
      ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U)) ≫
        ℱ.map i
[PROOFSTEP]
simp only [← ℱ.map_comp]
  -- Porting note : `congr` does not work, but `congr 1` does
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
j✝ : CostructuredArrow (Opens.map (𝟙 Y)).op U
⊢ ℱ.map
      ((IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op V.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            ((CostructuredArrow.map i).obj j✝)).left ≫
        eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V)) =
    ℱ.map
      ((IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            j✝).left ≫
        eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U) ≫ i)
[PROOFSTEP]
congr 1
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ (Opens.map (𝟙 Y)).op.obj (op U) = op U
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ NatTrans.app (id ℱ).inv (op U) =
    colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U))
      (CostructuredArrow.mk (eqToHom (_ : (Opens.map (𝟙 Y)).op.obj (op U) = op U)))
[PROOFSTEP]
rw [← Category.id_comp ((id ℱ).inv.app (op U)), ← NatIso.app_inv, Iso.comp_inv_eq]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ 𝟙 (ℱ.obj (op U)) =
    colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U))
        (CostructuredArrow.mk (eqToHom (_ : (Opens.map (𝟙 Y)).op.obj (op U) = op U))) ≫
      ((id ℱ).app (op U)).hom
[PROOFSTEP]
dsimp [id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ 𝟙 (ℱ.obj (op U)) =
    colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U)) (CostructuredArrow.mk (𝟙 (op ((Opens.map (𝟙 Y)).obj U)))) ≫
      colimit.desc (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U))
          (coconeOfDiagramTerminal
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U))) ≫
        ℱ.map
          (eqToHom
            (_ : op { carrier := ↑(𝟙 Y) '' ↑(op U).unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑(op U).unop)) } = op U))
[PROOFSTEP]
erw [colimit.ι_desc_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ 𝟙 (ℱ.obj (op U)) =
    NatTrans.app
        (coconeOfDiagramTerminal
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U))).ι
        (CostructuredArrow.mk (𝟙 (op ((Opens.map (𝟙 Y)).obj U)))) ≫
      ℱ.map
        (eqToHom
          (_ : op { carrier := ↑(𝟙 Y) '' ↑(op U).unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑(op U).unop)) } = op U))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ 𝟙 (ℱ.obj (op U)) =
    ℱ.map
        (IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            (CostructuredArrow.mk (𝟙 (op ((Opens.map (𝟙 Y)).obj U))))).left ≫
      ℱ.map
        (eqToHom
          (_ : op { carrier := ↑(𝟙 Y) '' ↑(op U).unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑(op U).unop)) } = op U))
[PROOFSTEP]
rw [← ℱ.map_comp, ← ℱ.map_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ ℱ.map (𝟙 (op U)) =
    ℱ.map
      ((IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            (CostructuredArrow.mk (𝟙 (op ((Opens.map (𝟙 Y)).obj U))))).left ≫
        eqToHom
          (_ : op { carrier := ↑(𝟙 Y) '' ↑(op U).unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑(op U).unop)) } = op U))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
⊢ pushforward C (𝟙 X) = 𝟭 (Presheaf C X)
[PROOFSTEP]
apply CategoryTheory.Functor.ext
[GOAL]
case h_map
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
⊢ autoParam
    (∀ (X_1 Y : Presheaf C X) (f : X_1 ⟶ Y),
      (pushforward C (𝟙 X)).map f =
        eqToHom (_ : ?F.obj X_1 = ?G.obj X_1) ≫
          (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj Y = (pushforward C (𝟙 X)).obj Y))
    _auto✝
[PROOFSTEP]
intros a b f
[GOAL]
case h_map
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
⊢ (pushforward C (𝟙 X)).map f =
    eqToHom (_ : ?F.obj a = ?G.obj a) ≫
      (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b)
[PROOFSTEP]
ext U
[GOAL]
case h_map.w
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
U : Opens ↑X
⊢ NatTrans.app ((pushforward C (𝟙 X)).map f) (op U) =
    NatTrans.app
      (eqToHom (_ : ?F.obj a = ?G.obj a) ≫
        (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b))
      (op U)
[PROOFSTEP]
erw [NatTrans.congr f (Opens.op_map_id_obj (op U))]
[GOAL]
case h_map.w
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
U : Opens ↑X
⊢ a.map (eqToHom (_ : (Opens.map (𝟙 X)).op.obj (op U) = op U)) ≫
      NatTrans.app f (op U) ≫ b.map (eqToHom (_ : op U = (Opens.map (𝟙 X)).op.obj (op U))) =
    NatTrans.app
      (eqToHom (_ : ?F.obj a = ?G.obj a) ≫
        (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b))
      (op U)
case h_obj
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
⊢ ∀ (X_1 : Presheaf C X), (pushforward C (𝟙 X)).obj X_1 = (𝟭 (Presheaf C X)).obj X_1
[PROOFSTEP]
simp only [Functor.op_obj, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id, Category.id_comp,
  Functor.id_obj, Functor.id_map]
[GOAL]
case h_obj
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
⊢ ∀ (X_1 : Presheaf C X), (pushforward C (𝟙 X)).obj X_1 = (𝟭 (Presheaf C X)).obj X_1
[PROOFSTEP]
apply Pushforward.id_eq
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ U = (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj U.unop))
[PROOFSTEP]
simp [Opens.map, Set.preimage_preimage]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (toPushforwardOfIso H₁ H₂) U =
    ℱ.map
        (eqToHom
          (_ :
            U =
              op
                {
                  carrier :=
                    ↑H₁.hom ⁻¹'
                      ↑(op { carrier := ↑H₁.inv ⁻¹' ↑U.unop, is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop,
                  is_open' :=
                    (_ :
                      IsOpen
                        (↑H₁.hom ⁻¹'
                          ↑(op
                                { carrier := ↑H₁.inv ⁻¹' ↑U.unop,
                                  is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop)) })) ≫
      NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop))
[PROOFSTEP]
delta toPushforwardOfIso
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (↑(Adjunction.homEquiv (Equivalence.toAdjunction (presheafEquivOfIso C H₁)) ℱ 𝒢) H₂) U =
    ℱ.map
        (eqToHom
          (_ :
            U =
              op
                {
                  carrier :=
                    ↑H₁.hom ⁻¹'
                      ↑(op { carrier := ↑H₁.inv ⁻¹' ↑U.unop, is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop,
                  is_open' :=
                    (_ :
                      IsOpen
                        (↑H₁.hom ⁻¹'
                          ↑(op
                                { carrier := ↑H₁.inv ⁻¹' ↑U.unop,
                                  is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop)) })) ≫
      NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop))
[PROOFSTEP]
simp only [pushforwardObj_obj, Functor.op_obj, Equivalence.toAdjunction, Adjunction.homEquiv_unit, Functor.id_obj,
  Functor.comp_obj, Adjunction.mkOfUnitCounit_unit, unop_op, eqToHom_map]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (NatTrans.app (Equivalence.unit (presheafEquivOfIso C H₁)) ℱ ≫ (presheafEquivOfIso C H₁).inverse.map H₂)
      U =
    eqToHom (_ : ℱ.obj U = ℱ.obj (op ((Opens.map H₁.hom).obj ((Opens.map H₁.inv).obj U.unop)))) ≫
      NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop))
[PROOFSTEP]
rw [NatTrans.comp_app, presheafEquivOfIso_inverse_map_app, Equivalence.Equivalence_mk'_unit]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (NatTrans.app (presheafEquivOfIso C H₁).unitIso.hom ℱ) U ≫
      NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop)) =
    eqToHom (_ : ℱ.obj U = ℱ.obj (op ((Opens.map H₁.hom).obj ((Opens.map H₁.inv).obj U.unop)))) ≫
      NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (NatTrans.app (presheafEquivOfIso C H₁).unitIso.hom ℱ) U =
    eqToHom (_ : ℱ.obj U = ℱ.obj (op ((Opens.map H₁.hom).obj ((Opens.map H₁.inv).obj U.unop))))
[PROOFSTEP]
simp only [Equivalence.unit, Equivalence.op, CategoryTheory.Equivalence.symm, Opens.mapMapIso, Functor.id_obj,
  Functor.comp_obj, Iso.symm_hom, NatIso.op_inv, Iso.symm_inv, NatTrans.op_app, NatIso.ofComponents_hom_app,
  eqToIso.hom, eqToHom_op, Equivalence.Equivalence_mk'_unitInv, Equivalence.Equivalence_mk'_counitInv, NatIso.op_hom,
  unop_op, op_unop, eqToIso.inv, NatIso.ofComponents_inv_app, eqToHom_unop, ← ℱ.map_comp, eqToHom_trans, eqToHom_map,
  presheafEquivOfIso_unitIso_hom_app_app]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C Y
𝒢 : Presheaf C X
H₂ : ℱ ⟶ H₁.hom _* 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj U.unop)) = U
[PROOFSTEP]
simp [Opens.map, Set.preimage_preimage]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C Y
𝒢 : Presheaf C X
H₂ : ℱ ⟶ H₁.hom _* 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (pushforwardToOfIso H₁ H₂) U =
    NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop)) ≫
      𝒢.map
        (eqToHom
          (_ :
            op
                {
                  carrier :=
                    ↑H₁.hom ⁻¹'
                      ↑(op { carrier := ↑H₁.inv ⁻¹' ↑U.unop, is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop,
                  is_open' :=
                    (_ :
                      IsOpen
                        (↑H₁.hom ⁻¹'
                          ↑(op
                                { carrier := ↑H₁.inv ⁻¹' ↑U.unop,
                                  is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop)) } =
              U))
[PROOFSTEP]
simp [pushforwardToOfIso, Equivalence.toAdjunction, CategoryStruct.comp]
