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))
F G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.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₁
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) f) :
          (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) f) :
          (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
        t :
      CC (obj (stalkFunctor C x) G))
rcases :
  ∀ (U₂ : Opens (↑X : Type v)) (hxU₂ : x ∈ U₂) (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) f) :
              (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) f) :
              (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:
rcases exists_germ_eq F t with ⟨U₂, hxU₂, t, rfl⟩

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))
F G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.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₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
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) f) :
          (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) f) :
          (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) (f.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) (f.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))
F G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.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₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
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) (f.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) (f.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) (iWU₁ : W ⟶ U₁) (iWU₂ : W ⟶ U₂)
    (heq :
      Eq (α := CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map iWU₁.op) : (a : CC (G.obj (op U₁))) → CC (G.obj (op W)))
            ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.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 iWU₂.op) : (a : CC (G.obj (op U₂))) → CC (G.obj (op W)))
            ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.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, iWU₁, iWU₂, heq⟩ := G.germ_eq x hxU₁ hxU₂ _ _ hst

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))
F G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.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₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
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) (f.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) (f.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
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  Eq (α := CC (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map iWU₁.op) : (a : CC (G.obj (op U₁))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.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 iWU₂.op) : (a : CC (G.obj (op U₂))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.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 (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op W)) : (a : CC (F.obj (op W))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU₁.op) : (a : CC (F.obj (op U₁))) → CC (F.obj (op W))) s :
          CC (F.obj (op W))) :
      CC (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op W)) : (a : CC (F.obj (op W))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU₂.op) : (a : CC (F.obj (op U₂))) → CC (F.obj (op W))) t :
          CC (F.obj (op W))) :
      CC (G.obj (op W)))

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, ← f.naturality, ← f.naturality,
    ConcreteCategory.comp_apply, ConcreteCategory.comp_apply] at heq

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.NatTrans.naturality
-- 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))
F G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.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₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
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) (f.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) (f.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
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  Eq (α := CC (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op W)) : (a : CC (F.obj (op W))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU₁.op) : (a : CC (F.obj (op U₁))) → CC (F.obj (op W))) s :
          CC (F.obj (op W))) :
      CC (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op W)) : (a : CC (F.obj (op W))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU₂.op) : (a : CC (F.obj (op U₂))) → CC (F.obj (op W))) t :
          CC (F.obj (op W))) :
      CC (G.obj (op W)))
⊢ Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map 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 iWU₂.op) : (a : CC (F.obj (op U₂))) → CC (F.obj (op W))) t :
      CC (F.obj (op W)))

Tactic:
replace heq := h W heq
-- 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))
F G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.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₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
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) (f.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) (f.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
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map 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 iWU₂.op) : (a : CC (F.obj (op U₂))) → CC (F.obj (op W))) t :
      CC (F.obj (op W)))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU₁.op) : (a : CC (F.obj (op U₁))) → CC (F.obj (op W))) s :
          CC (F.obj (op W))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU₂.op) : (a : CC (F.obj (op U₂))) → CC (F.obj (op W))) t :
          CC (F.obj (op W))) :
      CC (F.stalk x))

Tactic:
congr_arg (F.germ _ x hxW) heq

Premises used: CategoryTheory.ConcreteCategory.hom, TopCat.Presheaf.germ, congr_arg, DFunLike.coe
-- 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))
F G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.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₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
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) (f.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) (f.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
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map 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 iWU₂.op) : (a : CC (F.obj (op U₂))) → CC (F.obj (op W))) t :
      CC (F.obj (op W)))
e_1 : CC (obj (stalkFunctor C x) F) = 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 W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU₁.op) : (a : CC (F.obj (op U₁))) → CC (F.obj (op W))) s :
          CC (F.obj (op W))) :
      CC (F.stalk x))

Tactic:
(F.germ_res_apply iWU₁ x hxW s).symm

Premises used: TopCat.Presheaf.germ_res_apply, TopCat.Presheaf.stalk, Eq.symm
-- 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))
F G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.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₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
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) (f.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) (f.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
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map 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 iWU₂.op) : (a : CC (F.obj (op U₂))) → CC (F.obj (op W))) t :
      CC (F.obj (op W)))
e_1 : CC (obj (stalkFunctor C x) F) = 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)) t :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU₂.op) : (a : CC (F.obj (op U₂))) → CC (F.obj (op W))) t :
          CC (F.obj (op W))) :
      CC (F.stalk x))

Tactic:
(F.germ_res_apply iWU₂ x hxW t).symm

Premises used: TopCat.Presheaf.germ_res_apply, TopCat.Presheaf.stalk, Eq.symm
-- 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))
F G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.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₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
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) (f.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) (f.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
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map 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 iWU₂.op) : (a : CC (F.obj (op U₂))) → CC (F.obj (op W))) t :
      CC (F.obj (op W)))
e_1 : CC (obj (stalkFunctor C x) F) = 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 W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU₁.op) : (a : CC (F.obj (op U₁))) → CC (F.obj (op W))) s :
          CC (F.obj (op W))) :
      CC (F.stalk x))

Tactic:
exacts [(F.germ_res_apply iWU₁ x hxW s).symm, (F.germ_res_apply iWU₂ x hxW t).symm]

Premises used: TopCat.Presheaf.germ_res_apply, Eq.symm