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 : Presheaf C X
x : (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (F.stalk x)
obtain :
  ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U) (s : ToType (FC := FC) (CC := CC) (F.obj (op U))),
    ∃ (U_1 : Opens (↑X : Type v)) (m : x ∈ U_1) (_ : U_1 ∈ B) (s_1 : ToType (FC := FC) (CC := CC) (F.obj (op U_1))),
      Eq (α := CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U_1 x m) : (a : CC (F.obj (op U_1))) → CC (F.stalk x))
            s_1 :
          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)) s :
          CC (F.stalk x))
⊢ ∃ (U : Opens (↑X : Type v)) (m : x ∈ U) (_ : U ∈ B) (s : ToType (FC := FC) (CC := CC) (F.obj (op U))),
    (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x m) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s = t

Tactic:
obtain ⟨U, hxU, s, rfl⟩ := F.exists_germ_eq t

Premises used: TopCat.Presheaf.exists_germ_eq, rfl
-- 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 : Presheaf C X
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU : x ∈ U
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
obtain :
  ∀ (V : Opens (↑X : Type v)) (hV : V ∈ B) (hxV : x ∈ (↑V : Set (↑X : Type v)))
    (hVU : (↑V : Set (↑X : Type v)) ⊆ (↑U : Set (↑X : Type v))),
    ∃ (U_1 : Opens (↑X : Type v)) (m : x ∈ U_1) (_ : U_1 ∈ B) (s_1 : ToType (FC := FC) (CC := CC) (F.obj (op U_1))),
      Eq (α := CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U_1 x m) : (a : CC (F.obj (op U_1))) → CC (F.stalk x))
            s_1 :
          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)) s :
          CC (F.stalk x))
⊢ ∃ (U_1 : Opens (↑X : Type v)) (m : x ∈ U_1) (_ : U_1 ∈ B) (s_1 : ToType (FC := FC) (CC := CC) (F.obj (op U_1))),
    Eq (α := CC (F.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U_1 x m) : (a : CC (F.obj (op U_1))) → CC (F.stalk x)) s_1 :
        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)) s :
        CC (F.stalk x))

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := hB.exists_subset_of_mem_open hxU U.2

Premises used: TopologicalSpace.Opens.is_open', rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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 : Presheaf C X
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU : x ∈ U
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
V : Opens (↑X : Type v)
hV : V ∈ B
hxV : x ∈ (↑V : Set (↑X : Type v))
hVU : (↑V : Set (↑X : Type v)) ⊆ (↑U : Set (↑X : Type v))
rw :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.map
                ((homOfLE (x := (↑V : Set (↑X : Type v))) (y := (↑U : Set (↑X : Type v))) hVU).op (X :=
                  (↑V : Set (↑X : Type v))) (Y := (↑U : Set (↑X : Type v)))) ≫
              F.germ V x hxV) :
          (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)) s :
      CC (F.stalk x))
rw₁ rw₂ :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x ⋯) : (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)) s :
      CC (F.stalk x))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x hxV) : (a : CC (F.obj (op V))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC)
                (F.map
                  ((homOfLE (x := (↑V : Set (↑X : Type v))) (y := (↑U : Set (↑X : Type v))) hVU).op (X :=
                    (↑V : Set (↑X : Type v))) (Y := (↑U : Set (↑X : Type v))))) :
              (a : CC (F.obj (op U))) → CC (F.obj (op V)))
            s :
          CC (F.obj (op V))) :
      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)) s :
      CC (F.stalk x))

Tactic:
rw [← ConcreteCategory.comp_apply, F.germ_res']

Premises used: TopCat.Presheaf.germ_res', CategoryTheory.ConcreteCategory.comp_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 : Presheaf C X
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU : x ∈ U
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
V : Opens (↑X : Type v)
hV : V ∈ B
hxV : x ∈ (↑V : Set (↑X : Type v))
hVU : (↑V : Set (↑X : Type v)) ⊆ (↑U : Set (↑X : Type v))
⊢ ∃ (U_1 : Opens (↑X : Type v)) (m : x ∈ U_1) (_ : U_1 ∈ B) (s_1 : ToType (FC := FC) (CC := CC) (F.obj (op U_1))),
    Eq (α := CC (F.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U_1 x m) : (a : CC (F.obj (op U_1))) → CC (F.stalk x)) s_1 :
        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)) s :
        CC (F.stalk x))

Tactic:
exact ⟨V, hxV, hV, F.map (homOfLE hVU).op s, by rw [← ConcreteCategory.comp_apply, F.germ_res']⟩
-- 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 : Presheaf C X
U V : Opens (↑X : Type v)
x : (↑X : Type v)
mU : x ∈ U
mV : x ∈ V
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
t : ToType (FC := FC) (CC := CC) (F.obj (op V))
h :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x mU) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x mV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) t :
      CC (F.stalk x))
obtain :
  ∀ (W : Opens (↑X : Type v)) (hxW : x ∈ W) (hWU : W ⟶ U) (hWV : W ⟶ V)
    (e :
      Eq (α := CC (F.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map hWU.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 hWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) t :
          CC (F.obj (op W)))),
    ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (_ : W ∈ B) (hWU : W ≤ U) (hWV : W ≤ V),
      Eq (α := CC (F.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hWU).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 hWV).op) :
              (a : CC (F.obj (op V))) → CC (F.obj (op W)))
            t :
          CC (F.obj (op W)))
⊢ ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (_ : W ∈ B) (hWU : W ≤ U) (hWV : W ≤ V),
    Eq (α := CC (F.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hWU).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 hWV).op) :
            (a : CC (F.obj (op V))) → CC (F.obj (op W)))
          t :
        CC (F.obj (op W)))

Tactic:
obtain ⟨W, hxW, hWU, hWV, e⟩ := F.germ_eq x mU mV _ _ h

Premises used: TopCat.Presheaf.germ_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))
B : Set (Opens (↑X : Type v))
hB : Opens.IsBasis B
F : Presheaf C X
U V : Opens (↑X : Type v)
x : (↑X : Type v)
mU : x ∈ U
mV : x ∈ V
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
t : ToType (FC := FC) (CC := CC) (F.obj (op V))
h :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x mU) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x mV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) t :
      CC (F.stalk x))
W : Opens (↑X : Type v)
hxW : x ∈ W
hWU : W ⟶ U
hWV : W ⟶ V
e :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map hWU.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 hWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) t :
      CC (F.obj (op W)))
obtain :
  ∀ (W' : Opens (↑X : Type v)) (hW' : W' ∈ B) (hxW' : x ∈ (↑W' : Set (↑X : Type v)))
    (hW'W : (↑W' : Set (↑X : Type v)) ⊆ (↑W : Set (↑X : Type v))),
    ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (_ : W ∈ B) (hWU : W ≤ U) (hWV : W ≤ V),
      Eq (α := CC (F.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hWU).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 hWV).op) :
              (a : CC (F.obj (op V))) → CC (F.obj (op W)))
            t :
          CC (F.obj (op W)))
⊢ ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (_ : W ∈ B) (hWU : W ≤ U) (hWV : W ≤ V),
    Eq (α := CC (F.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hWU).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 hWV).op) :
            (a : CC (F.obj (op V))) → CC (F.obj (op W)))
          t :
        CC (F.obj (op W)))

Tactic:
obtain ⟨_, ⟨W', hW', rfl⟩, hxW', hW'W⟩ := hB.exists_subset_of_mem_open hxW W.2

Premises used: TopologicalSpace.Opens.is_open', rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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 : Presheaf C X
U V : Opens (↑X : Type v)
x : (↑X : Type v)
mU : x ∈ U
mV : x ∈ V
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
t : ToType (FC := FC) (CC := CC) (F.obj (op V))
h :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x mU) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x mV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) t :
      CC (F.stalk x))
W : Opens (↑X : Type v)
hxW : x ∈ W
hWU : W ⟶ U
hWV : W ⟶ V
e :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map hWU.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 hWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) t :
      CC (F.obj (op W)))
W' : Opens (↑X : Type v)
hW' : W' ∈ B
hxW' : x ∈ (↑W' : Set (↑X : Type v))
hW'W : (↑W' : Set (↑X : Type v)) ⊆ (↑W : Set (↑X : Type v))
⊢ ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (_ : W ∈ B) (hWU : W ≤ U) (hWV : W ≤ V),
    Eq (α := CC (F.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hWU).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 hWV).op) :
            (a : CC (F.obj (op V))) → CC (F.obj (op W)))
          t :
        CC (F.obj (op W)))

Tactic:
⟨W', hxW', hW', hW'W.trans hWU.le, hW'W.trans hWV.le, ?_⟩

Premises used: Quiver.Hom.le, HasSubset.Subset.trans, 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))
B : Set (Opens (↑X : Type v))
hB : Opens.IsBasis B
F : Presheaf C X
U V : Opens (↑X : Type v)
x : (↑X : Type v)
mU : x ∈ U
mV : x ∈ V
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
t : ToType (FC := FC) (CC := CC) (F.obj (op V))
h :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x mU) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x mV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) t :
      CC (F.stalk x))
W : Opens (↑X : Type v)
hxW : x ∈ W
hWU : W ⟶ U
hWV : W ⟶ V
e :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map hWU.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 hWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) t :
      CC (F.obj (op W)))
W' : Opens (↑X : Type v)
hW' : W' ∈ B
hxW' : x ∈ (↑W' : Set (↑X : Type v))
hW'W : (↑W' : Set (↑X : Type v)) ⊆ (↑W : Set (↑X : Type v))
refine :
  Eq (α := CC (F.obj (op W')))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).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 ⋯).op) : (a : CC (F.obj (op V))) → CC (F.obj (op W')))
        t :
      CC (F.obj (op W')))
⊢ ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (_ : W ∈ B) (hWU : W ≤ U) (hWV : W ≤ V),
    Eq (α := CC (F.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hWU).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 hWV).op) :
            (a : CC (F.obj (op V))) → CC (F.obj (op W)))
          t :
        CC (F.obj (op W)))

Tactic:
refine ⟨W', hxW', hW', hW'W.trans hWU.le, hW'W.trans hWV.le, ?_⟩
-- 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 : Presheaf C X
U V : Opens (↑X : Type v)
x : (↑X : Type v)
mU : x ∈ U
mV : x ∈ V
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
t : ToType (FC := FC) (CC := CC) (F.obj (op V))
h :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x mU) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x mV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) t :
      CC (F.stalk x))
W : Opens (↑X : Type v)
hxW : x ∈ W
hWU : W ⟶ U
hWV : W ⟶ V
e :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map hWU.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 hWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) t :
      CC (F.obj (op W)))
W' : Opens (↑X : Type v)
hW' : W' ∈ B
hxW' : x ∈ (↑W' : Set (↑X : Type v))
hW'W : (↑W' : Set (↑X : Type v)) ⊆ (↑W : Set (↑X : Type v))
⊢ Eq (α := CC (F.obj (op W')))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).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 ⋯).op) : (a : CC (F.obj (op V))) → CC (F.obj (op W')))
        t :
      CC (F.obj (op W')))

Tactic:
simpa only [← ConcreteCategory.comp_apply, ← F.map_comp] using
    DFunLike.congr_arg (ConcreteCategory.hom (F.map (homOfLE hW'W).op)) e

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, CategoryTheory.homOfLE, CategoryTheory.Functor.map_comp, DFunLike.congr_arg
-- 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)
s t : CC (obj (stalkFunctor C x) F)
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))
        s :
      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))
        t :
      CC (obj (stalkFunctor C x) G))
obtain :
  ∀ (U₁ : Opens (↑X : Type v)) (hxU₁ : x ∈ U₁) (hU₁ : U₁ ∈ B) (s : 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))
            t :
          CC (obj (stalkFunctor C x) G))),
    (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s = t
⊢ s = t

Tactic:
obtain ⟨U₁, hxU₁, hU₁, s, rfl⟩ := exists_mem_germ_eq_of_isBasis hB _ x s

Premises used: TopCat.Presheaf.exists_mem_germ_eq_of_isBasis, rfl
-- 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)
t : CC (obj (stalkFunctor C x) F)
U₁ : Opens (↑X : Type v)
hxU₁ : x ∈ U₁
hU₁ : U₁ ∈ B
s : 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))
        t :
      CC (obj (stalkFunctor C x) G))
obtain :
  ∀ (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) 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))
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s = t

Tactic:
obtain ⟨U₂, hxU₂, hU₂, t, rfl⟩ := exists_mem_germ_eq_of_isBasis hB _ x t

Premises used: TopCat.Presheaf.exists_mem_germ_eq_of_isBasis, rfl