-- Mathlib/Topology/Sheaves/LocallySurjective.lean
theorem locally_surjective_iff_surjective_on_stalks (T : ℱ ⟶ 𝒢) :
    IsLocallySurjective T ↔ ∀ x : X, Function.Surjective ((stalkFunctor C x).map T)

Proof state:
case h.e'_2.h
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
V : Opens ↑X
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) = t_x
e_1✝ : CC (𝒢.stalk x) = CC ((stalkFunctor C x).obj 𝒢)
⊢ (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) =
    (ConcreteCategory.hom (𝒢.germ V x hxV)) ((ConcreteCategory.hom (T.app (op V))) s)

Tactic:
convert stalkFunctor_map_germ_apply _ _ _ _ s

Result:
no goals

Proof state:
case mpr.imageSieve_mem
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1

Tactic:
set t_x := 𝒢.germ _ x hxU t with ht_x

Result:
case mpr.imageSieve_mem
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1

Proof state:
case mpr.imageSieve_mem.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
V : Opens ↑X
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  (ConcreteCategory.hom (𝒢.map hWV.op)) ((ConcreteCategory.hom (T.app (op V))) s) =
    (ConcreteCategory.hom (𝒢.map hWU.op)) t
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1

Tactic:
refine ⟨W, hWU, ⟨ℱ.map hWV.op s, ?_⟩, hxW⟩

Result:
case mpr.imageSieve_mem.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
V : Opens ↑X
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  (ConcreteCategory.hom (𝒢.map hWV.op)) ((ConcreteCategory.hom (T.app (op V))) s) =
    (ConcreteCategory.hom (𝒢.map hWU.op)) t
⊢ (ConcreteCategory.hom (T.app (op W))) ((ConcreteCategory.hom (ℱ.map hWV.op)) s) =
    (ConcreteCategory.hom (𝒢.map hWU.op)) t

Proof state:
case mpr.imageSieve_mem.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
V : Opens ↑X
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) = t_x
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1

Tactic:
have key_W := 𝒢.germ_eq x hxV hxU (T.app _ s) t <| by
  convert hs_x using 1
  symm
  convert stalkFunctor_map_germ_apply _ _ _ _ s

Result:
case mpr.imageSieve_mem.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
V : Opens ↑X
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) = t_x
key_W :
  ∃ W,
    ∃ (_ : x ∈ W),
      ∃ iU iV,
        (ConcreteCategory.hom (𝒢.map iU.op)) ((ConcreteCategory.hom (T.app (op V))) s) =
          (ConcreteCategory.hom (𝒢.map iV.op)) t
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1

Proof state:
case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
⊢ IsLocallySurjective T

Tactic:
constructor

Result:
case mpr.imageSieve_mem
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
⊢ ∀ {U : Opens ↑X} (s : ToType (𝒢.obj (op U))), Presheaf.imageSieve T s ∈ (Opens.grothendieckTopology ↑X) U