awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
B : Set (Opens (↑X : Type v))
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα :
  ∀ U ∈ B,
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U))) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
x : (↑X : Type v)
U₁ : Opens (↑X : Type v)
hxU₁ : x ∈ U₁
hU₁ : U₁ ∈ B
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
hU₂ : U₂ ∈ B
t : ToType (FC := FC) (CC := CC) (F.obj (op U₂))
hst :
  Eq (α := CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) α) :
          (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s :
          CC (F.stalk x)) :
      CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) α) :
          (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₂ x hxU₂) : (a : CC (F.obj (op U₂))) → CC (F.stalk x)) t :
          CC (F.stalk x)) :
      CC (obj (stalkFunctor C x) G))
⊢ Eq (α := CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₁ x hxU₁) : (a : CC (G.obj (op U₁))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₁)) : (a : CC (F.obj (op U₁))) → CC (G.obj (op U₁)))
            s :
          CC (G.obj (op U₁))) :
      CC (G.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₂ x hxU₂) : (a : CC (G.obj (op U₂))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₂)) : (a : CC (F.obj (op U₂))) → CC (G.obj (op U₂)))
            t :
          CC (G.obj (op U₂))) :
      CC (G.stalk x))

Tactic:
rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply] at hst

Premises used: TopCat.Presheaf.stalkFunctor_map_germ_apply
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
B : Set (Opens (↑X : Type v))
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα :
  ∀ U ∈ B,
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U))) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
x : (↑X : Type v)
U₁ : Opens (↑X : Type v)
hxU₁ : x ∈ U₁
hU₁ : U₁ ∈ B
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
hU₂ : U₂ ∈ B
t : ToType (FC := FC) (CC := CC) (F.obj (op U₂))
hst :
  Eq (α := CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₁ x hxU₁) : (a : CC (G.obj (op U₁))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₁)) : (a : CC (F.obj (op U₁))) → CC (G.obj (op U₁)))
            s :
          CC (G.obj (op U₁))) :
      CC (G.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₂ x hxU₂) : (a : CC (G.obj (op U₂))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₂)) : (a : CC (F.obj (op U₂))) → CC (G.obj (op U₂)))
            t :
          CC (G.obj (op U₂))) :
      CC (G.stalk x))
obtain :
  ∀ (W : Opens (↑X : Type v)) (hxW : x ∈ W) (hW : W ∈ B) (iWU₁ : W ≤ U₁) (iWU₂ : W ≤ U₂)
    (heq :
      Eq (α := CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE iWU₁).op) :
              (a : CC (G.obj (op U₁))) → CC (G.obj (op W)))
            ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₁)) :
                  (a : CC (F.obj (op U₁))) → CC (G.obj (op U₁)))
                s :
              CC (G.obj (op U₁))) :
          CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE iWU₂).op) :
              (a : CC (G.obj (op U₂))) → CC (G.obj (op W)))
            ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₂)) :
                  (a : CC (F.obj (op U₂))) → CC (G.obj (op U₂)))
                t :
              CC (G.obj (op U₂))) :
          CC (G.obj (op W)))),
    Eq (α := CC (obj (stalkFunctor C x) F))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s :
        CC (F.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₂ x hxU₂) : (a : CC (F.obj (op U₂))) → CC (F.stalk x)) t :
        CC (F.stalk x))
⊢ Eq (α := CC (obj (stalkFunctor C x) F))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₂ x hxU₂) : (a : CC (F.obj (op U₂))) → CC (F.stalk x)) t :
      CC (F.stalk x))

Tactic:
obtain ⟨W, hxW, hW, iWU₁, iWU₂, heq⟩ := germ_eq_of_isBasis hB _ _ hxU₁ hxU₂ hst

Premises used: TopCat.Presheaf.germ_eq_of_isBasis
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
B : Set (Opens (↑X : Type v))
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα :
  ∀ U ∈ B,
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U))) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
x : (↑X : Type v)
U₁ : Opens (↑X : Type v)
hxU₁ : x ∈ U₁
hU₁ : U₁ ∈ B
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
hU₂ : U₂ ∈ B
t : ToType (FC := FC) (CC := CC) (F.obj (op U₂))
hst :
  Eq (α := CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₁ x hxU₁) : (a : CC (G.obj (op U₁))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₁)) : (a : CC (F.obj (op U₁))) → CC (G.obj (op U₁)))
            s :
          CC (G.obj (op U₁))) :
      CC (G.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₂ x hxU₂) : (a : CC (G.obj (op U₂))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₂)) : (a : CC (F.obj (op U₂))) → CC (G.obj (op U₂)))
            t :
          CC (G.obj (op U₂))) :
      CC (G.stalk x))
W : Opens (↑X : Type v)
hxW : x ∈ W
hW : W ∈ B
iWU₁ : W ≤ U₁
iWU₂ : W ≤ U₂
heq :
  Eq (α := CC (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE iWU₁).op) :
          (a : CC (G.obj (op U₁))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₁)) : (a : CC (F.obj (op U₁))) → CC (G.obj (op U₁)))
            s :
          CC (G.obj (op U₁))) :
      CC (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE iWU₂).op) :
          (a : CC (G.obj (op U₂))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₂)) : (a : CC (F.obj (op U₂))) → CC (G.obj (op U₂)))
            t :
          CC (G.obj (op U₂))) :
      CC (G.obj (op W)))
⊢ Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE iWU₁).op) :
          (a : CC (F.obj (op U₁))) → CC (F.obj (op W)))
        s :
      CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE iWU₂).op) :
          (a : CC (F.obj (op U₂))) → CC (F.obj (op W)))
        t :
      CC (F.obj (op W)))

Tactic:
simp only [← α.naturality_apply, (hα W hW).eq_iff] at heq

Premises used: CategoryTheory.NatTrans.naturality_apply, Function.Injective.eq_iff
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
B : Set (Opens (↑X : Type v))
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα :
  ∀ U ∈ B,
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U))) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
x : (↑X : Type v)
U₁ : Opens (↑X : Type v)
hxU₁ : x ∈ U₁
hU₁ : U₁ ∈ B
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
hU₂ : U₂ ∈ B
t : ToType (FC := FC) (CC := CC) (F.obj (op U₂))
hst :
  Eq (α := CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₁ x hxU₁) : (a : CC (G.obj (op U₁))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₁)) : (a : CC (F.obj (op U₁))) → CC (G.obj (op U₁)))
            s :
          CC (G.obj (op U₁))) :
      CC (G.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₂ x hxU₂) : (a : CC (G.obj (op U₂))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.app (op U₂)) : (a : CC (F.obj (op U₂))) → CC (G.obj (op U₂)))
            t :
          CC (G.obj (op U₂))) :
      CC (G.stalk x))
W : Opens (↑X : Type v)
hxW : x ∈ W
hW : W ∈ B
iWU₁ : W ≤ U₁
iWU₂ : W ≤ U₂
heq :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE iWU₁).op) :
          (a : CC (F.obj (op U₁))) → CC (F.obj (op W)))
        s :
      CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE iWU₂).op) :
          (a : CC (F.obj (op U₂))) → CC (F.obj (op W)))
        t :
      CC (F.obj (op W)))
⊢ Eq (α := CC (obj (stalkFunctor C x) F))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₂ x hxU₂) : (a : CC (F.obj (op U₂))) → CC (F.stalk x)) t :
      CC (F.stalk x))

Tactic:
simpa [germ_res_apply'] using congr(F.germ W x hxW $heq)

Premises used: TopCat.Presheaf.germ_res_apply'
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
U : Opens (↑X : Type v)
s t :
  ToType (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
h :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Eq (α := CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          s :
        CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          t :
        CC (F.presheaf.stalk x))
choose :
  ∀ (V : (x : ↥U) → Opens (↑X : Type v)) (m : ∀ (x : ↥U), (↑x : (↑X : Type v)) ∈ V x) (i₁ i₂ : (x : ↥U) → V x ⟶ U)
    (heq :
      ∀ (x : ↥U),
        Eq (α := CC (F.presheaf.obj (op (V x))))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₁ x).op) :
                (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
              s :
            CC (F.presheaf.obj (op (V x))))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₂ x).op) :
                (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
              t :
            CC (F.presheaf.obj (op (V x))))),
    s = t
⊢ s = t

Tactic:
choose V m i₁ i₂ heq using fun x : U => F.presheaf.germ_eq x.1 x.2 x.2 s t (h x.1 x.2)

Premises used: TopCat.Presheaf.germ_eq, TopCat.Sheaf.presheaf, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
U : Opens (↑X : Type v)
s t :
  ToType (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
h :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Eq (α := CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          s :
        CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          t :
        CC (F.presheaf.stalk x))
V : (x : ↥U) → Opens (↑X : Type v)
m : ∀ (x : ↥U), (↑x : (↑X : Type v)) ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U),
    Eq (α := CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₁ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          s :
        CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₂ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          t :
        CC (F.presheaf.obj (op (V x))))
hcover : U ≤ iSup V
h₁ :
  ∀ (i : ↥U),
    Eq (α :=
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (i₁ i).op) :
            (a : CC (F.obj.obj (op U))) → CC (F.obj.obj (op (V i))))
          s :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (i₁ i).op) :
            (a : CC (F.obj.obj (op U))) → CC (F.obj.obj (op (V i))))
          t :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V i))))
⊢ s = t

Tactic:
apply F.eq_of_locally_eq' V U i₁

Premises used: TopCat.Sheaf.eq_of_locally_eq'
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
U : Opens (↑X : Type v)
s t :
  ToType (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
h :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Eq (α := CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          s :
        CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          t :
        CC (F.presheaf.stalk x))
V : (x : ↥U) → Opens (↑X : Type v)
m : ∀ (x : ↥U), (↑x : (↑X : Type v)) ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U),
    Eq (α := CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₁ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          s :
        CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₂ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          t :
        CC (F.presheaf.obj (op (V x))))
x : (↑X : Type v)
hxU : x ∈ U
hcover : ∃ (i : ↥U), x ∈ V i
⊢ x ∈ iSup V

Tactic:
simp only [Opens.mem_iSup]

Premises used: TopologicalSpace.Opens.mem_iSup
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
U : Opens (↑X : Type v)
s t :
  ToType (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
h :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Eq (α := CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          s :
        CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          t :
        CC (F.presheaf.stalk x))
V : (x : ↥U) → Opens (↑X : Type v)
m : ∀ (x : ↥U), (↑x : (↑X : Type v)) ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U),
    Eq (α := CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₁ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          s :
        CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₂ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          t :
        CC (F.presheaf.obj (op (V x))))
x : (↑X : Type v)
hxU : x ∈ U
⊢ ∃ (i : ↥U), x ∈ V i

Tactic:
⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
U : Opens (↑X : Type v)
s t :
  ToType (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
h :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Eq (α := CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          s :
        CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          t :
        CC (F.presheaf.stalk x))
V : (x : ↥U) → Opens (↑X : Type v)
m : ∀ (x : ↥U), (↑x : (↑X : Type v)) ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U),
    Eq (α := CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₁ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          s :
        CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₂ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          t :
        CC (F.presheaf.obj (op (V x))))
x : (↑X : Type v)
hxU : x ∈ U
⊢ ∃ (i : ↥U), x ∈ V i

Tactic:
exact ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
G : Presheaf C X
f : F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))) ⟶ G
⊢ (∀ (x : (↑X : Type v)),
      Function.Injective.{v + 1, v + 1} (α :=
        CC
          (obj (stalkFunctor C x)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
        (β := CC (obj (stalkFunctor C x) G))
        (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f)) :
          (a : CC ((stalkFunctor C x).obj F.obj)) → CC ((stalkFunctor C x).obj G))) ↔
    ∀ (U : Opens (↑X : Type v)),
      Function.Injective.{v + 1, v + 1} (α :=
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))) (β :=
        CC (G.obj (op U)))
        (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U))) : (a : CC (F.obj.obj (op U))) → CC (G.obj (op U)))

Tactic:
⟨fun h U => app_injective_of_stalkFunctor_map_injective f U fun x _ => h x,
    stalkFunctor_map_injective_of_app_injective⟩

Premises used: TopCat.Presheaf.stalkFunctor_map_injective_of_app_injective, TopCat.Presheaf.app_injective_of_stalkFunctor_map_injective, Iff.intro