-- Mathlib/Topology/Sheaves/Stalks.lean
theorem stalkPushforward_iso_of_isInducing {f : X ⟶ Y} (hf : IsInducing f)
    (F : X.Presheaf C) (x : X) : IsIso (F.stalkPushforward _ f x)

Proof state:
case h.e'_5.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
this : (OpenNhds.map f x).Initial
e_3✝ :
  ((pushforward C f).obj F).stalk ((ConcreteCategory.hom f) x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4✝ : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ F.germ ((Opens.map f).obj U) x hU =
    ((pushforward C f).obj F).germ U ((ConcreteCategory.hom f) x) hU ≫
      (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).hom

Tactic:
symm

Result:
case h.e'_5.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
this : (OpenNhds.map f x).Initial
e_3✝ :
  ((pushforward C f).obj F).stalk ((ConcreteCategory.hom f) x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4✝ : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ ((pushforward C f).obj F).germ U ((ConcreteCategory.hom f) x) hU ≫
      (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).hom =
    F.germ ((Opens.map f).obj U) x hU

Proof state:
case h.e'_5.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
this : (OpenNhds.map f x).Initial
e_3✝ :
  ((pushforward C f).obj F).stalk ((ConcreteCategory.hom f) x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4✝ : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ ((pushforward C f).obj F).germ U ((ConcreteCategory.hom f) x) hU ≫
      (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).hom =
    F.germ ((Opens.map f).obj U) x hU

Tactic:
exact colimit.ι_pre ((OpenNhds.inclusion x).op ⋙ F) (OpenNhds.map f x).op _

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
this : (OpenNhds.map f x).Initial
⊢ IsIso (stalkPushforward C f F x)

Tactic:
convert (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).isIso_hom

Result:
case h.e'_5.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
this : (OpenNhds.map f x).Initial
e_3✝ :
  ((pushforward C f).obj F).stalk ((ConcreteCategory.hom f) x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4✝ : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
⊢ stalkPushforward C f F x = (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
⊢ IsIso (stalkPushforward C f F x)

Tactic:
haveI := Functor.initial_of_adjunction (hf.adjunctionNhds x)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
this : (OpenNhds.map f x).Initial
⊢ IsIso (stalkPushforward C f F x)

Proof state:
case h.e'_5.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
this : (OpenNhds.map f x).Initial
e_3✝ :
  ((pushforward C f).obj F).stalk ((ConcreteCategory.hom f) x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4✝ : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
⊢ stalkPushforward C f F x = (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).hom

Tactic:
refine stalk_hom_ext _ fun U hU ↦ (stalkPushforward_germ _ f F _ x hU).trans ?_

Result:
case h.e'_5.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
this : (OpenNhds.map f x).Initial
e_3✝ :
  ((pushforward C f).obj F).stalk ((ConcreteCategory.hom f) x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4✝ : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ F.germ ((Opens.map f).obj U) x hU =
    ((pushforward C f).obj F).germ U ((ConcreteCategory.hom f) x) hU ≫
      (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).hom