case mk
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y✝ Z : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : stalk F x ⟶ Y
ih :
  ∀ (U : Opens ↑X) (hxU : x ∈ U), germ F { val := x, property := hxU } ≫ f₁ = germ F { val := x, property := hxU } ≫ f₂
U : OpenNhds x
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
        { unop := U } ≫
      f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
        { unop := U } ≫
      f₂
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y✝ Z : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : stalk F x ⟶ Y
ih :
  ∀ (U : Opens ↑X) (hxU : x ∈ U), germ F { val := x, property := hxU } ≫ f₁ = germ F { val := x, property := hxU } ≫ f₂
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F) U ≫ f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F) U ≫ f₂
induction' U using Opposite.rec with U
case mk.mk
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y✝ Z : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : stalk F x ⟶ Y
ih :
  ∀ (U : Opens ↑X) (hxU : x ∈ U), germ F { val := x, property := hxU } ≫ f₁ = germ F { val := x, property := hxU } ≫ f₂
U : Opens ↑X
hxU : x ∈ U
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
        { unop := { obj := U, property := hxU } } ≫
      f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
        { unop := { obj := U, property := hxU } } ≫
      f₂
case mk
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y✝ Z : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : stalk F x ⟶ Y
ih :
  ∀ (U : Opens ↑X) (hxU : x ∈ U), germ F { val := x, property := hxU } ≫ f₁ = germ F { val := x, property := hxU } ≫ f₂
U : OpenNhds x
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
        { unop := U } ≫
      f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
        { unop := U } ≫
      f₂
cases' U with U hxU
no goals
case mk.mk
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y✝ Z : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : stalk F x ⟶ Y
ih :
  ∀ (U : Opens ↑X) (hxU : x ∈ U), germ F { val := x, property := hxU } ≫ f₁ = germ F { val := x, property := hxU } ≫ f₂
U : Opens ↑X
hxU : x ∈ U
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
        { unop := { obj := U, property := hxU } } ≫
      f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
        { unop := { obj := U, property := hxU } } ≫
      f₂
exact ih U hxU