case intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
t : (forget C).obj ((stalkFunctor C x).obj F)
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
hst :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) t
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = t
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
s t : (forget C).obj ((stalkFunctor C x).obj F)
hst : (forget C).map ((stalkFunctor C x).map f) s = (forget C).map ((stalkFunctor C x).map f) t
⊢ s = t
rcases germ_exist F x s with ⟨U₁, hxU₁, s, rfl⟩
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
case intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
t : (forget C).obj ((stalkFunctor C x).obj F)
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
hst :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) t
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = t
rcases germ_exist F x t with ⟨U₂, hxU₂, t, rfl⟩
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
erw [stalkFunctor_map_germ_apply _ ⟨x, _⟩] at hst
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
erw [stalkFunctor_map_germ_apply _ ⟨x, _⟩] at hst
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  (forget C).map (G.map iWU₁.op) ((forget C).map (f.app U₁.op) s) =
    (forget C).map (G.map iWU₂.op) ((forget C).map (f.app U₂.op) t)
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
obtain ⟨W, hxW, iWU₁, iWU₂, heq⟩ := G.germ_eq x hxU₁ hxU₂ _ _ hst
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  (forget C).map (f.app W.op) ((forget C).map (F.map iWU₁.op) s) =
    (forget C).map (f.app W.op) ((forget C).map (F.map iWU₂.op) t)
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  (forget C).map (G.map iWU₁.op) ((forget C).map (f.app U₁.op) s) =
    (forget C).map (G.map iWU₂.op) ((forget C).map (f.app U₂.op) t)
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
rw [← comp_apply, ← comp_apply, ← f.naturality, ← f.naturality, comp_apply, comp_apply] at heq
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq : (forget C).map (F.map iWU₁.op) s = (forget C).map (F.map iWU₂.op) t
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  (forget C).map (f.app W.op) ((forget C).map (F.map iWU₁.op) s) =
    (forget C).map (f.app W.op) ((forget C).map (F.map iWU₂.op) t)
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
replace heq := h W heq
case h.e'_2.h
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq : (forget C).map (F.map iWU₁.op) s = (forget C).map (F.map iWU₂.op) t
e_1✝ : (forget C).obj ((stalkFunctor C x).obj F) = (forget C).obj (stalk F ↑{ val := x, property := hxW })
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s =
    (forget C).map (germ F { val := x, property := hxW }) ((forget C).map (F.map iWU₁.op) s)

case h.e'_3.h
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq : (forget C).map (F.map iWU₁.op) s = (forget C).map (F.map iWU₂.op) t
e_1✝ : (forget C).obj ((stalkFunctor C x).obj F) = (forget C).obj (stalk F ↑{ val := x, property := hxW })
⊢ (forget C).map (germ F { val := x, property := hxU₂ }) t =
    (forget C).map (germ F { val := x, property := hxW }) ((forget C).map (F.map iWU₂.op) t)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq : (forget C).map (F.map iWU₁.op) s = (forget C).map (F.map iWU₂.op) t
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s = (forget C).map (germ F { val := x, property := hxU₂ }) t
convert congr_arg (F.germ ⟨x, hxW⟩) heq using 1
no goals
case h.e'_2.h
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq : (forget C).map (F.map iWU₁.op) s = (forget C).map (F.map iWU₂.op) t
e_1✝ : (forget C).obj ((stalkFunctor C x).obj F) = (forget C).obj (stalk F ↑{ val := x, property := hxW })
⊢ (forget C).map (germ F { val := x, property := hxU₁ }) s =
    (forget C).map (germ F { val := x, property := hxW }) ((forget C).map (F.map iWU₁.op) s)

case h.e'_3.h
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ((forget C).map (f.app U.op))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : (forget C).obj (F.obj U₁.op)
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : (forget C).obj (F.obj U₂.op)
hst✝¹ :
  (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₁ }) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst✝ :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map ((stalkFunctor C x).map f) ((forget C).map (germ F { val := x, property := hxU₂ }) t)
hst :
  (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₁ }) ⋙ G)
        { obj := U₁, property := (_ : ↑{ val := x, property := hxU₁ } ∈ U₁) }.op)
      ((forget C).map (f.app U₁.op) s) =
    (forget C).map
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑{ val := x, property := hxU₂ }) ⋙ G)
        { obj := U₂, property := (_ : ↑{ val := x, property := hxU₂ } ∈ U₂) }.op)
      ((forget C).map (f.app U₂.op) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq : (forget C).map (F.map iWU₁.op) s = (forget C).map (F.map iWU₂.op) t
e_1✝ : (forget C).obj ((stalkFunctor C x).obj F) = (forget C).obj (stalk F ↑{ val := x, property := hxW })
⊢ (forget C).map (germ F { val := x, property := hxU₂ }) t =
    (forget C).map (germ F { val := x, property := hxW }) ((forget C).map (F.map iWU₂.op) t)
exacts [(F.germ_res_apply iWU₁ ⟨x, hxW⟩ s).symm, (F.germ_res_apply iWU₂ ⟨x, hxW⟩ t).symm]