awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T (↑x_1 : (↑X : Type u_1))
hU : P.toPrelocalPredicate (T := T).pred (T := T) fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T (↑x_1 : (↑X : Type u_1))
hV : P.toPrelocalPredicate (T := T).pred (T := T) fV
h :
  Eq (α := T x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P.cocone (T := T) x).ι.app U) :
          (a : { f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop U))) → T (↑x_1 : (↑X : Type u_1)) // P.pred f }) →
            (P.cocone x).pt)
        (Subtype.mk (p := fun (f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop U))) → T (↑x_1 : (↑X : Type u_1))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) fU hU) :
      (P.cocone (T := T) x).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P.cocone (T := T) x).ι.app V) :
          (a : { f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop V))) → T (↑x_1 : (↑X : Type u_1)) // P.pred f }) →
            (P.cocone x).pt)
        (Subtype.mk (p := fun (f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop V))) → T (↑x_1 : (↑X : Type u_1))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) fV hV) :
      (P.cocone (T := T) x).pt)
W : Opens (↑X : Type u_1)
m : x ∈ W
iU : Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m ⟶ unop U
iV : Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m ⟶ unop V
w :
  ∀ (w : ↥(↑(Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m) : Opens (↑X : Type u_1))),
    Eq (α :=
      T (↑((iU : (a : ↥(↑⟨W, m⟩ : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w) : (↑X : Type u_1)))
      (fU ((iU : (a : ↥(↑⟨W, m⟩ : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w))
      (fV ((iV : (a : ↥(↑⟨W, m⟩ : Opens (↑X : Type u_1))) → ↥(↑(unop V) : Opens (↑X : Type u_1))) w))
⊢ (↑(unop (op (Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m))) : Opens (↑X : Type u_1)) ⟶
    (↑(unop U) : Opens (↑X : Type u_1))

Tactic:
exact iU
-- 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
T : ℱ ⟶ 𝒢
⊢ IsLocallySurjective (FC := FC) (CC := CC) T ↔
    ∀ (U : Opens (↑X : Type v)) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
      ∀ x ∈ U,
        ∃ (V : Opens (↑X : Type v)) (x_1 : V ≤ U),
          (∃ (s : CC (ℱ.obj (op V))),
              (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
                  s =
                restrictOpen (FC := FC) (CC := CC) t V x_1) ∧
            x ∈ V

Tactic:
⟨fun h _ t x hx ↦ ?_, fun h => ⟨fun s x hx ↦ ?_⟩⟩

Premises used: CategoryTheory.Presheaf.IsLocallySurjective.mk, Iff.intro
-- 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
T : ℱ ⟶ 𝒢
refine_1 :
  ∀ (h : IsLocallySurjective (FC := FC) (CC := CC) T) (x : Opens (↑X : Type v))
    (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op x))) (x_1 : (↑X : Type v)) (hx : x_1 ∈ x),
    ∃ (V : Opens (↑X : Type v)) (x_2 : V ≤ x),
      (∃ (s : CC (ℱ.obj (op V))),
          (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s =
            restrictOpen (FC := FC) (CC := CC) t V x_2) ∧
        x_1 ∈ V
refine_2 :
  ∀
    (h :
      ∀ (U : Opens (↑X : Type v)) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
        ∀ x ∈ U,
          ∃ (V : Opens (↑X : Type v)) (x_1 : V ≤ U),
            (∃ (s : CC (ℱ.obj (op V))),
                (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) :
                      (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
                    s =
                  restrictOpen (FC := FC) (CC := CC) t V x_1) ∧
              x ∈ V)
    {U : Opens (↑X : Type v)} (s : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))) (x : (↑X : Type v)) (hx : x ∈ U),
    ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T s).arrows f ∧ x ∈ U_1
⊢ IsLocallySurjective (FC := FC) (CC := CC) T ↔
    ∀ (U : Opens (↑X : Type v)) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
      ∀ x ∈ U,
        ∃ (V : Opens (↑X : Type v)) (x_1 : V ≤ U),
          (∃ (s : CC (ℱ.obj (op V))),
              (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
                  s =
                restrictOpen (FC := FC) (CC := CC) t V x_1) ∧
            x ∈ V

Tactic:
refine ⟨fun h _ t x hx ↦ ?_, fun h => ⟨fun s x hx ↦ ?_⟩⟩
-- 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
T : ℱ ⟶ 𝒢
h : IsLocallySurjective (FC := FC) (CC := CC) T
x_1 : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op x_1))
x : (↑X : Type v)
hx : x ∈ x_1
refine_1 :
  ∀ (V : Opens (↑X : Type v)) (i : V ⟶ x_1) (hi : (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows i ∧ x ∈ V),
    ∃ (V : Opens (↑X : Type v)) (x_2 : V ≤ x_1),
      (∃ (s : CC (ℱ.obj (op V))),
          (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s =
            restrictOpen (FC := FC) (CC := CC) t V x_2) ∧
        x ∈ V
⊢ ∃ (V : Opens (↑X : Type v)) (x_2 : V ≤ x_1),
    (∃ (s : CC (ℱ.obj (op V))),
        (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s =
          restrictOpen (FC := FC) (CC := CC) t V x_2) ∧
      x ∈ V

Tactic:
obtain ⟨V, i, hi⟩ := h.imageSieve_mem t x hx

Premises used: CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem
-- 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
T : ℱ ⟶ 𝒢
h : IsLocallySurjective (FC := FC) (CC := CC) T
x_1 : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op x_1))
x : (↑X : Type v)
hx : x ∈ x_1
V : Opens (↑X : Type v)
i : V ⟶ x_1
hi : (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows i ∧ x ∈ V
⊢ ∃ (V : Opens (↑X : Type v)) (x_2 : V ≤ x_1),
    (∃ (s : CC (ℱ.obj (op V))),
        (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s =
          restrictOpen (FC := FC) (CC := CC) t V x_2) ∧
      x ∈ V

Tactic:
⟨V, leOfHom i, hi⟩

Premises used: Exists.intro, CategoryTheory.leOfHom
-- 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
T : ℱ ⟶ 𝒢
h : IsLocallySurjective (FC := FC) (CC := CC) T
x_1 : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op x_1))
x : (↑X : Type v)
hx : x ∈ x_1
V : Opens (↑X : Type v)
i : V ⟶ x_1
hi : (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows i ∧ x ∈ V
⊢ ∃ (V : Opens (↑X : Type v)) (x_2 : V ≤ x_1),
    (∃ (s : CC (ℱ.obj (op V))),
        (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s =
          restrictOpen (FC := FC) (CC := CC) t V x_2) ∧
      x ∈ V

Tactic:
exact ⟨V, leOfHom i, hi⟩
-- 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
T : ℱ ⟶ 𝒢
h :
  ∀ (U : Opens (↑X : Type v)) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
    ∀ x ∈ U,
      ∃ (V : Opens (↑X : Type v)) (x_1 : V ≤ U),
        (∃ (s : CC (ℱ.obj (op V))),
            (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
                s =
              restrictOpen (FC := FC) (CC := CC) t V x_1) ∧
          x ∈ V
U : Opens (↑X : Type v)
s : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hx : x ∈ U
refine_2 :
  ∀ (V : Opens (↑X : Type v)) (Vle : V ≤ U)
    (hV :
      (∃ (s_1 : CC (ℱ.obj (op V))),
          (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
              s_1 =
            restrictOpen (FC := FC) (CC := CC) s V Vle) ∧
        x ∈ V),
    ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T s).arrows f ∧ x ∈ U_1
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T s).arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨V, Vle, hV⟩ := h _ s x hx
-- 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
T : ℱ ⟶ 𝒢
h :
  ∀ (U : Opens (↑X : Type v)) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
    ∀ x ∈ U,
      ∃ (V : Opens (↑X : Type v)) (x_1 : V ≤ U),
        (∃ (s : CC (ℱ.obj (op V))),
            (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
                s =
              restrictOpen (FC := FC) (CC := CC) t V x_1) ∧
          x ∈ V
U : Opens (↑X : Type v)
s : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hx : x ∈ U
V : Opens (↑X : Type v)
Vle : V ≤ U
hV :
  (∃ (s_1 : CC (ℱ.obj (op V))),
      (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s_1 =
        restrictOpen (FC := FC) (CC := CC) s V Vle) ∧
    x ∈ V
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T s).arrows f ∧ x ∈ U_1

Tactic:
⟨V, homOfLE Vle, hV⟩

Premises used: CategoryTheory.homOfLE, Exists.intro
-- 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
T : ℱ ⟶ 𝒢
h :
  ∀ (U : Opens (↑X : Type v)) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
    ∀ x ∈ U,
      ∃ (V : Opens (↑X : Type v)) (x_1 : V ≤ U),
        (∃ (s : CC (ℱ.obj (op V))),
            (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
                s =
              restrictOpen (FC := FC) (CC := CC) t V x_1) ∧
          x ∈ V
U : Opens (↑X : Type v)
s : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hx : x ∈ U
V : Opens (↑X : Type v)
Vle : V ≤ U
hV :
  (∃ (s_1 : CC (ℱ.obj (op V))),
      (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s_1 =
        restrictOpen (FC := FC) (CC := CC) s V Vle) ∧
    x ∈ V
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T s).arrows f ∧ x ∈ U_1

Tactic:
exact ⟨V, homOfLE Vle, hV⟩
-- 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 : ℱ ⟶ 𝒢
mp :
  IsLocallySurjective (FC := FC) (CC := CC) T →
    ∀ (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 𝒢))
mpr :
  (∀ (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 𝒢))) →
    IsLocallySurjective (FC := FC) (CC := CC) T
⊢ IsLocallySurjective (FC := FC) (CC := CC) T ↔
    ∀ (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 𝒢))

Tactic:
constructor
-- 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 : IsLocallySurjective (FC := FC) (CC := CC) T
x : (↑X : Type v)
g : CC (Functor.obj (stalkFunctor C x) 𝒢)
mp :
  ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
    ∃ (a : CC (Functor.obj (stalkFunctor C x) ℱ)),
      Eq (α := 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 𝒢))
            a :
          CC (Functor.obj (stalkFunctor C x) 𝒢))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
          CC (𝒢.stalk x))
⊢ ∃ (a : 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 𝒢))
        a =
      g

Tactic:
obtain ⟨U, hxU, t, rfl⟩ := 𝒢.exists_germ_eq g

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 : IsLocallySurjective (FC := FC) (CC := CC) T
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU : x ∈ U
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
mp :
  ∀ (V : Opens (↑X : Type v)) (ι : V ⟶ U) (hxV : x ∈ V) (s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V)))
    (h_eq :
      Eq (α := CC (𝒢.obj (op V)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map ι.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op V))) t :
          CC (𝒢.obj (op V)))),
    ∃ (a : CC (Functor.obj (stalkFunctor C x) ℱ)),
      Eq (α := 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 𝒢))
            a :
          CC (Functor.obj (stalkFunctor C x) 𝒢))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
          CC (𝒢.stalk x))
⊢ ∃ (a : CC (Functor.obj (stalkFunctor C x) ℱ)),
    Eq (α := 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 𝒢))
          a :
        CC (Functor.obj (stalkFunctor C x) 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
        CC (𝒢.stalk x))

Tactic:
rcases hT.imageSieve_mem t x hxU with ⟨V, ι, ⟨s, h_eq⟩, hxV⟩

Premises used: CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem
-- 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 : IsLocallySurjective (FC := FC) (CC := CC) T
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU : x ∈ U
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
V : Opens (↑X : Type v)
ι : V ⟶ U
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
h_eq :
  Eq (α := CC (𝒢.obj (op V)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
      CC (𝒢.obj (op V)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map ι.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op V))) t :
      CC (𝒢.obj (op V)))
h :
  Eq (α := 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 𝒢))
        ((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 U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
      CC (𝒢.stalk x))
⊢ ∃ (a : CC (Functor.obj (stalkFunctor C x) ℱ)),
    Eq (α := 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 𝒢))
          a :
        CC (Functor.obj (stalkFunctor C x) 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
        CC (𝒢.stalk x))

Tactic:
use ℱ.germ _ x hxV s

Premises used: CategoryTheory.ConcreteCategory.hom, TopCat.Presheaf.germ, DFunLike.coe
-- 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 : IsLocallySurjective (FC := FC) (CC := CC) T
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU : x ∈ U
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
V : Opens (↑X : Type v)
ι : V ⟶ U
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
h_eq :
  Eq (α := CC (𝒢.obj (op V)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
      CC (𝒢.obj (op V)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map ι.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op V))) t :
      CC (𝒢.obj (op V)))
⊢ Eq (α := 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 𝒢))
        ((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 U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
      CC (𝒢.stalk x))

Tactic:
simp [h_eq, germ_res_apply]

Premises used: TopCat.Presheaf.germ_res_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 𝒢))
mpr :
  ∀ {U : Opens (↑X : Type v)} (s : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
    Presheaf.imageSieve (FA := FC) (CA := CC) T s ∈
      (Opens.grothendieckTopology (↑X : Type v) : (a : Opens (↑X : Type v)) → Set (Sieve a)) U
⊢ IsLocallySurjective (FC := FC) (CC := CC) T

Tactic:
constructor
-- 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
⊢ let t_x : CC (𝒢.stalk x) :=
    (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t;
  t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t

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

Premises used: CategoryTheory.ConcreteCategory.hom, TopCat.Presheaf.germ, DFunLike.coe