awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
mpr :
  ∀ (s_x : CC (Functor.obj (stalkFunctor C x) ℱ))
    (hs_x :
      (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
            (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
          s_x =
        t_x),
    ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨s_x, hs_x : ((stalkFunctor C x).map T) s_x = t_x⟩ := hT x t_x
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
s_x : CC (Functor.obj (stalkFunctor C x) ℱ)
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      s_x =
    t_x
mpr :
  ∀ (V : Opens (↑X : Type v)) (hxV : x ∈ V) (s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V)))
    (hs_x :
      (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
            (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
            CC (ℱ.stalk x)) =
        t_x),
    ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨V, hxV, s, rfl⟩ := ℱ.exists_germ_eq s_x

Premises used: TopCat.Presheaf.exists_germ_eq, rfl
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x

Tactic:
hs_x
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
h :
  CC (𝒢.stalk x) = CC (Functor.obj (stalkFunctor C x) 𝒢) →
    Eq (α := CC (𝒢.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ V x hxV) : (a : CC (𝒢.obj (op V))) → CC (𝒢.stalk x))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
            CC (𝒢.obj (op V))) :
        CC (𝒢.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
            (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
            CC (ℱ.stalk x)) :
        CC (Functor.obj (stalkFunctor C x) 𝒢))
⊢ Eq (α := CC (𝒢.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ V x hxV) : (a : CC (𝒢.obj (op V))) → CC (𝒢.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
      CC (𝒢.stalk x))

Tactic:
convert! hs_x using 1
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
e_1 : CC (𝒢.stalk x) = CC (Functor.obj (stalkFunctor C x) 𝒢)
h :
  Eq (α := CC (𝒢.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
          (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
          CC (ℱ.stalk x)) :
      CC (Functor.obj (stalkFunctor C x) 𝒢))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ V x hxV) : (a : CC (𝒢.obj (op V))) → CC (𝒢.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.stalk x))
⊢ Eq (α := CC (𝒢.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ V x hxV) : (a : CC (𝒢.obj (op V))) → CC (𝒢.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
          (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
          CC (ℱ.stalk x)) :
      CC (Functor.obj (stalkFunctor C x) 𝒢))

Tactic:
symm
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
e_1 : CC (𝒢.stalk x) = CC (Functor.obj (stalkFunctor C x) 𝒢)
⊢ Eq (α := ToType (FC := FC) (CC := CC) (Functor.obj (stalkFunctor C x) 𝒢))
    ((ConcreteCategory.hom (FC := FC) (CC := ToType (FC := FC) (CC := CC))
            (CategoryTheory.Functor.map (stalkFunctor C x) T) :
          (a : ToType ((stalkFunctor C x).obj ℱ)) → ToType ((stalkFunctor C x).obj 𝒢))
        ((ConcreteCategory.hom (FC := FC) (CC := ToType (FC := FC) (CC := CC)) (ℱ.germ V x hxV) :
              (a : ToType (ℱ.obj (op V))) → ToType (ℱ.stalk x))
            s :
          ToType (FC := FC) (CC := CC) (ℱ.stalk x)) :
      ToType (FC := FC) (CC := CC) (Functor.obj (stalkFunctor C x) 𝒢))
    ((ConcreteCategory.hom (FC := FC) (CC := ToType (FC := FC) (CC := CC)) (𝒢.germ V x hxV) :
          (a : ToType (𝒢.obj (op V))) → ToType (𝒢.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := ToType (FC := FC) (CC := CC)) (T.app (op V)) :
              (a : ToType (ℱ.obj (op V))) → ToType (𝒢.obj (op V)))
            s :
          ToType (FC := FC) (CC := CC) (𝒢.obj (op V))) :
      ToType (FC := FC) (CC := CC) (𝒢.stalk x))

Tactic:
stalkFunctor_map_germ_apply _ _ _ _ s

Premises used: TopCat.Presheaf.stalkFunctor_map_germ_apply
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
e_1 : CC (𝒢.stalk x) = CC (Functor.obj (stalkFunctor C x) 𝒢)
⊢ Eq (α := CC (𝒢.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
          (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
          CC (ℱ.stalk x)) :
      CC (Functor.obj (stalkFunctor C x) 𝒢))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ V x hxV) : (a : CC (𝒢.obj (op V))) → CC (𝒢.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.stalk x))

Tactic:
convert! stalkFunctor_map_germ_apply _ _ _ _ s

Premises used: TopCat.Presheaf.stalkFunctor_map_germ_apply
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
⊢ ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (iU : W ⟶ V) (iV : W ⟶ U),
    Eq (α := CC (𝒢.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map iU.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
            CC (𝒢.obj (op V))) :
        CC (𝒢.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map iV.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
        CC (𝒢.obj (op W)))

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
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
key_W :
  ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (iU : W ⟶ V) (iV : W ⟶ U),
    Eq (α := CC (𝒢.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map iU.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
            CC (𝒢.obj (op V))) :
        CC (𝒢.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map iV.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
        CC (𝒢.obj (op W)))
mpr :
  ∀ (W : Opens (↑X : Type v)) (hxW : x ∈ W) (hWV : W ⟶ V) (hWU : W ⟶ U)
    (h_eq :
      Eq (α := CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
            ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
                s :
              CC (𝒢.obj (op V))) :
          CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
          CC (𝒢.obj (op W)))),
    ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨W, hxW, hWV, hWU, h_eq⟩ := key_W
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
W : Opens (↑X : Type v)
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1

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

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, And.intro, Exists.intro, DFunLike.coe