C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
⊢ ∃ a, (forget C).map (f.val.app U.op) a = t
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
⊢ Function.Surjective ((forget C).map (f.val.app U.op))
intro t
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
⊢ ∃ a, (forget C).map (f.val.app U.op) a = t
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
⊢ ∃ a, (forget C).map (f.val.app U.op) a = t
choose V mV iVU sf heq using hsurj t
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
⊢ ∃ a, (forget C).map (f.val.app U.op) a = t
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
⊢ ∃ a, (forget C).map (f.val.app U.op) a = t
have V_cover : U ≤ iSup V := by
  intro x hxU
  erw [Opens.mem_iSup]
  exact ⟨⟨x, hxU⟩, mV ⟨x, hxU⟩⟩
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
⊢ (forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x) =
    (forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y)
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
⊢ IsCompatible F.val V sf
intro x y
case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
⊢ ∀ (x_1 : { x_1 // x_1 ∈ V x ⊓ V y }),
    (forget C).map (germ (Sheaf.presheaf F) x_1) ((forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x)) =
      (forget C).map (germ (Sheaf.presheaf F) x_1) ((forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y))
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
⊢ (forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x) =
    (forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y)
apply section_ext
case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
z : { x_1 // x_1 ∈ V x ⊓ V y }
⊢ (forget C).map (germ (Sheaf.presheaf F) z) ((forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x)) =
    (forget C).map (germ (Sheaf.presheaf F) z) ((forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y))
case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
⊢ ∀ (x_1 : { x_1 // x_1 ∈ V x ⊓ V y }),
    (forget C).map (germ (Sheaf.presheaf F) x_1) ((forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x)) =
      (forget C).map (germ (Sheaf.presheaf F) x_1) ((forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y))
intro z
case h.a
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
z : { x_1 // x_1 ∈ V x ⊓ V y }
⊢ (forget C).map ((stalkFunctor C ↑{ val := ↑z, property := (_ : ↑z ∈ ↑U) }).map f.val)
      ((forget C).map (germ (Sheaf.presheaf F) z)
        ((forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x))) =
    (forget C).map ((stalkFunctor C ↑{ val := ↑z, property := (_ : ↑z ∈ ↑U) }).map f.val)
      ((forget C).map (germ (Sheaf.presheaf F) z) ((forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y)))
case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
z : { x_1 // x_1 ∈ V x ⊓ V y }
⊢ (forget C).map (germ (Sheaf.presheaf F) z) ((forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x)) =
    (forget C).map (germ (Sheaf.presheaf F) z) ((forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y))
apply hinj ⟨z, (iVU x).le ((inf_le_left : V x ⊓ V y ≤ V x) z.2)⟩
case h.a
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
z : { x_1 // x_1 ∈ V x ⊓ V y }
⊢ (forget C).map ((stalkFunctor C ↑z).map f.val)
      ((forget C).map (germ (Sheaf.presheaf F) z)
        ((forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x))) =
    (forget C).map ((stalkFunctor C ↑z).map f.val)
      ((forget C).map (germ (Sheaf.presheaf F) z) ((forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y)))
case h.a
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
z : { x_1 // x_1 ∈ V x ⊓ V y }
⊢ (forget C).map ((stalkFunctor C ↑{ val := ↑z, property := (_ : ↑z ∈ ↑U) }).map f.val)
      ((forget C).map (germ (Sheaf.presheaf F) z)
        ((forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x))) =
    (forget C).map ((stalkFunctor C ↑{ val := ↑z, property := (_ : ↑z ∈ ↑U) }).map f.val)
      ((forget C).map (germ (Sheaf.presheaf F) z) ((forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y)))
dsimp only
case h.a
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
z : { x_1 // x_1 ∈ V x ⊓ V y }
⊢ (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑z) ⋙ G.val) { obj := V x ⊓ V y, property := (_ : ↑z ∈ V x ⊓ V y) }.op)
      ((forget C).map (f.val.app (V x ⊓ V y).op) ((forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x))) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑z) ⋙ G.val) { obj := V x ⊓ V y, property := (_ : ↑z ∈ V x ⊓ V y) }.op)
      ((forget C).map (f.val.app (V x ⊓ V y).op) ((forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y)))
case h.a
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
z : { x_1 // x_1 ∈ V x ⊓ V y }
⊢ (forget C).map ((stalkFunctor C ↑z).map f.val)
      ((forget C).map (germ (Sheaf.presheaf F) z)
        ((forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x))) =
    (forget C).map ((stalkFunctor C ↑z).map f.val)
      ((forget C).map (germ (Sheaf.presheaf F) z) ((forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y)))
erw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply]
case h.a
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
z : { x_1 // x_1 ∈ V x ⊓ V y }
⊢ (forget C).map
      (G.val.map ((iVU x).op ≫ (Opens.infLELeft (V x) (V y)).op) ≫
        colimit.ι (Functor.op (OpenNhds.inclusion ↑z) ⋙ G.val)
          { obj := V x ⊓ V y, property := (_ : ↑z ∈ V x ⊓ V y) }.op)
      t =
    (forget C).map
      (G.val.map ((iVU y).op ≫ (Opens.infLERight (V x) (V y)).op) ≫
        colimit.ι (Functor.op (OpenNhds.inclusion ↑z) ⋙ G.val)
          { obj := V x ⊓ V y, property := (_ : ↑z ∈ V x ⊓ V y) }.op)
      t
case h.a
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
z : { x_1 // x_1 ∈ V x ⊓ V y }
⊢ (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑z) ⋙ G.val) { obj := V x ⊓ V y, property := (_ : ↑z ∈ V x ⊓ V y) }.op)
      ((forget C).map (f.val.app (V x ⊓ V y).op) ((forget C).map (F.val.map (Opens.infLELeft (V x) (V y)).op) (sf x))) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑z) ⋙ G.val) { obj := V x ⊓ V y, property := (_ : ↑z ∈ V x ⊓ V y) }.op)
      ((forget C).map (f.val.app (V x ⊓ V y).op) ((forget C).map (F.val.map (Opens.infLERight (V x) (V y)).op) (sf y)))
simp_rw [← comp_apply, f.1.naturality, comp_apply, heq, ← comp_apply, ← G.1.map_comp]
no goals
case h.a
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
x y : { x // x ∈ U }
z : { x_1 // x_1 ∈ V x ⊓ V y }
⊢ (forget C).map
      (G.val.map ((iVU x).op ≫ (Opens.infLELeft (V x) (V y)).op) ≫
        colimit.ι (Functor.op (OpenNhds.inclusion ↑z) ⋙ G.val)
          { obj := V x ⊓ V y, property := (_ : ↑z ∈ V x ⊓ V y) }.op)
      t =
    (forget C).map
      (G.val.map ((iVU y).op ≫ (Opens.infLERight (V x) (V y)).op) ≫
        colimit.ι (Functor.op (OpenNhds.inclusion ↑z) ⋙ G.val)
          { obj := V x ⊓ V y, property := (_ : ↑z ∈ V x ⊓ V y) }.op)
      t
rfl
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
x : ↑X
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup V)
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
⊢ U ≤ iSup V
intro x hxU
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
x : ↑X
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ V i
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
x : ↑X
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup V)
erw [Opens.mem_iSup]
no goals
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
x : ↑X
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ V i
exact ⟨⟨x, hxU⟩, mV ⟨x, hxU⟩⟩
case intro.intro
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
this : IsCompatible F.val V sf
s : (forget C).obj (F.val.obj U.op)
s_spec : ∀ (i : { x // x ∈ U }), (forget C).map (F.val.map (iVU i).op) s = sf i
⊢ ∃ a, (forget C).map (f.val.app U.op) a = t
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
this : IsCompatible F.val V sf
⊢ ∃ a, (forget C).map (f.val.app U.op) a = t
obtain ⟨s, s_spec, -⟩ := F.existsUnique_gluing' V U iVU V_cover sf this
case intro.intro
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
this : IsCompatible F.val V sf
s : (forget C).obj (F.val.obj U.op)
s_spec : ∀ (i : { x // x ∈ U }), (forget C).map (F.val.map (iVU i).op) s = sf i
⊢ (forget C).map (f.val.app U.op) s = t
case intro.intro
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
this : IsCompatible F.val V sf
s : (forget C).obj (F.val.obj U.op)
s_spec : ∀ (i : { x // x ∈ U }), (forget C).map (F.val.map (iVU i).op) s = sf i
⊢ ∃ a, (forget C).map (f.val.app U.op) a = t
use s
case intro.intro.h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
this : IsCompatible F.val V sf
s : (forget C).obj (F.val.obj U.op)
s_spec : ∀ (i : { x // x ∈ U }), (forget C).map (F.val.map (iVU i).op) s = sf i
⊢ ∀ (i : { x // x ∈ U }),
    (forget C).map (G.val.map (iVU i).op) ((forget C).map (f.val.app U.op) s) = (forget C).map (G.val.map (iVU i).op) t
case intro.intro
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
this : IsCompatible F.val V sf
s : (forget C).obj (F.val.obj U.op)
s_spec : ∀ (i : { x // x ∈ U }), (forget C).map (F.val.map (iVU i).op) s = sf i
⊢ (forget C).map (f.val.app U.op) s = t
apply G.eq_of_locally_eq' V U iVU V_cover
case intro.intro.h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
this : IsCompatible F.val V sf
s : (forget C).obj (F.val.obj U.op)
s_spec : ∀ (i : { x // x ∈ U }), (forget C).map (F.val.map (iVU i).op) s = sf i
x : { x // x ∈ U }
⊢ (forget C).map (G.val.map (iVU x).op) ((forget C).map (f.val.app U.op) s) = (forget C).map (G.val.map (iVU x).op) t
case intro.intro.h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
this : IsCompatible F.val V sf
s : (forget C).obj (F.val.obj U.op)
s_spec : ∀ (i : { x // x ∈ U }), (forget C).map (F.val.map (iVU i).op) s = sf i
⊢ ∀ (i : { x // x ∈ U }),
    (forget C).map (G.val.map (iVU i).op) ((forget C).map (f.val.app U.op) s) = (forget C).map (G.val.map (iVU i).op) t
intro x
no goals
case intro.intro.h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f.val))
hsurj :
  ∀ (t : (forget C).obj (G.val.obj U.op)) (x : { x // x ∈ U }),
    ∃ V x iVU s, (forget C).map (f.val.app V.op) s = (forget C).map (G.val.map iVU.op) t
t : (forget C).obj (G.val.obj U.op)
V : { x // x ∈ U } → Opens ↑X
mV : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
iVU : (x : { x // x ∈ U }) → V x ⟶ U
sf : (x : { x // x ∈ U }) → (forget C).obj (F.val.obj (V x).op)
heq : ∀ (x : { x // x ∈ U }), (forget C).map (f.val.app (V x).op) (sf x) = (forget C).map (G.val.map (iVU x).op) t
V_cover : U ≤ iSup V
this : IsCompatible F.val V sf
s : (forget C).obj (F.val.obj U.op)
s_spec : ∀ (i : { x // x ∈ U }), (forget C).map (F.val.map (iVU i).op) s = sf i
x : { x // x ∈ U }
⊢ (forget C).map (G.val.map (iVU x).op) ((forget C).map (f.val.app U.op) s) = (forget C).map (G.val.map (iVU x).op) t
rw [← comp_apply, ← f.1.naturality, comp_apply, s_spec, heq]