C✝ : Type u
inst✝² : Category C✝
X : TopCat
C : Type u_2
inst✝¹ : Category 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 V.op)
⊢ (forget C).map (e.app U.op) ((forget C).map (F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op) x) =
    (forget C).map (G.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op) ((forget C).map (e.app V.op) x)
C✝ : Type u
inst✝² : Category C✝
X : TopCat
C : Type u_2
inst✝¹ : Category 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 V.op)
⊢ (forget C).map (e.app U.op) (x |_ U) = (forget C).map (e.app V.op) x |_ U
delta restrictOpen restrict
no goals
C✝ : Type u
inst✝² : Category C✝
X : TopCat
C : Type u_2
inst✝¹ : Category 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 V.op)
⊢ (forget C).map (e.app U.op) ((forget C).map (F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op) x) =
    (forget C).map (G.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op) ((forget C).map (e.app V.op) x)
rw [← comp_apply, NatTrans.naturality, comp_apply]