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