awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
Y : C
w :
  ∀ (U : Opens (↑X : Type u)),
    Eq (α :=
      Functor.obj (Functor.obj (skyscraperPresheafFunctor p₀) Y) (op U) ⟶
        Functor.obj (Functor.obj (skyscraperPresheafFunctor p₀) Y) (op U))
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          Functor.obj (skyscraperPresheafFunctor p₀)
            (Functor.obj (C := Presheaf C X) (Presheaf.stalkFunctor C p₀)
              (Functor.obj (skyscraperPresheafFunctor p₀) Y)))
          (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) (Functor.obj (skyscraperPresheafFunctor p₀) Y))
          (CategoryTheory.Functor.map (skyscraperPresheafFunctor p₀)
            (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀) Y)))
        (op U))
      (NatTrans.app (𝟙 (Functor.obj (skyscraperPresheafFunctor p₀) Y)) (op U))
⊢ Eq (α :=
    Quiver.Hom (V := Presheaf C X) (Functor.obj (skyscraperPresheafFunctor p₀) Y)
      (Functor.obj (skyscraperPresheafFunctor p₀) Y))
    (CategoryStruct.comp (Y :=
      Functor.obj (skyscraperPresheafFunctor p₀)
        (Functor.obj (C := Presheaf C X) (Presheaf.stalkFunctor C p₀) (Functor.obj (skyscraperPresheafFunctor p₀) Y)))
      (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) (Functor.obj (skyscraperPresheafFunctor p₀) Y))
      (CategoryTheory.Functor.map (skyscraperPresheafFunctor p₀)
        (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀) Y)))
    (𝟙 (Functor.obj (skyscraperPresheafFunctor p₀) Y))

Tactic:
ext
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
Y : C
U : Opens (↑X : Type u)
h : p₀ ∈ U
pos :
  Eq.{u + 1} (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (𝟙 (if p₀ ∈ U then Y else terminal.{u, v} C)) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U))
⊢ Eq (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (CategoryStruct.comp (Y := if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)
        (Presheaf.germ (skyscraperPresheaf p₀ Y) U p₀ ⋯ ≫ eqToHom ⋯)
        (eqToHom ⋯ ≫
          CategoryStruct.comp (Y := Y)
            (Iso.hom
                (colimit.isoColimitCocone
                  { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y ⋯,
                    isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y ⋯ }) :
              Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ ⟶ Y)
            (eqToHom ⋯)) :
      (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U) :
      Functor.obj (skyscraperPresheaf p₀ Y) (op U) ⟶ Functor.obj (skyscraperPresheaf p₀ Y) (op U))

Tactic:
simp [Presheaf.germ]

Premises used: TopCat.Presheaf.germ
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
Y : C
U : Opens (↑X : Type u)
h : p₀ ∈ U
⊢ Eq.{u + 1} (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (𝟙 (if p₀ ∈ U then Y else terminal.{u, v} C)) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U))

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
Y : C
U : Opens (↑X : Type u)
h : p₀ ∉ U
neg :
  Eq.{u + 1} (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (𝟙 (if p₀ ∈ U then Y else terminal.{u, v} C)) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U))
⊢ Eq.{u + 1} (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C) ⋯)
        (if p₀ ∈ U then Y else terminal.{u, v} C) ≫
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ U then Y else terminal.{u, v} C) ⋯)
        (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C))
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U))

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
Y : C
U : Opens (↑X : Type u)
h : p₀ ∉ U
⊢ Eq.{u + 1} (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (𝟙 (if p₀ ∈ U then Y else terminal.{u, v} C)) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U))

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
⊢ Functor.IsRightAdjoint (C := Presheaf C X) (skyscraperPresheafFunctor p₀)

Tactic:
(skyscraperPresheafStalkAdjunction _).isRightAdjoint

Premises used: skyscraperPresheafStalkAdjunction, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
⊢ Functor.IsLeftAdjoint (C := Presheaf C X) (Presheaf.stalkFunctor C p₀)

Tactic:
have : ∀ U : Opens X, Decidable (p₀ ∈ U) := fun _ ↦ Classical.dec _
  (skyscraperPresheafStalkAdjunction _).isLeftAdjoint

Premises used: Membership.mem, skyscraperPresheafStalkAdjunction, Classical.dec, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
𝓐 𝓑 : TopCat.Sheaf C X
f : 𝓐 ⟶ 𝓑
⊢ Eq (α :=
    (Functor.obj (𝟭 (TopCat.Sheaf C X)) 𝓐).obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⟶
      (Functor.obj ((Sheaf.forget C X ⋙ Presheaf.stalkFunctor C p₀) ⋙ skyscraperSheafFunctor p₀) 𝓑).obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))))
    (InducedCategory.Hom.hom
      (CategoryTheory.Functor.map (𝟭 (TopCat.Sheaf C X)) f ≫
        {
          hom :=
            NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀)
              (𝓑.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u)))) }))
    (InducedCategory.Hom.hom
      ({
          hom :=
            NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀)
              (𝓐.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u)))) } ≫
        CategoryTheory.Functor.map ((Sheaf.forget C X ⋙ Presheaf.stalkFunctor C p₀) ⋙ skyscraperSheafFunctor p₀) f))

Tactic:
apply (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).naturality

Premises used: CategoryTheory.NatTrans.naturality, StalkSkyscraperPresheafAdjunctionAuxs.unit
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
⊢ Functor.IsLeftAdjoint (C := TopCat.Sheaf C X) (Sheaf.forget C X ⋙ Presheaf.stalkFunctor C p₀)

Tactic:
have : ∀ U : Opens X, Decidable (p₀ ∈ U) := fun _ ↦ Classical.dec _
  (stalkSkyscraperSheafAdjunction p₀).isLeftAdjoint

Premises used: stalkSkyscraperSheafAdjunction, Membership.mem, Classical.dec, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
⊢ Functor.IsRightAdjoint (C := TopCat.Sheaf C X) (skyscraperSheafFunctor p₀)

Tactic:
(stalkSkyscraperSheafAdjunction _).isRightAdjoint

Premises used: stalkSkyscraperSheafAdjunction, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
U : (Opens (↑X : Type u))ᵒᵖ
h : p₀ ∉ unop U
dsimp : IsTerminal.{u, v} (if p₀ ∈ unop U then A else terminal.{u, v} C)
⊢ IsTerminal.{u, v}
    (Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) (skyscraperSheaf p₀ A))
      U)

Tactic:
dsimp
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
U : (Opens (↑X : Type u))ᵒᵖ
h : p₀ ∉ unop U
rw : IsTerminal.{u, v} (terminal.{u, v} C)
⊢ IsTerminal.{u, v} (if p₀ ∈ unop U then A else terminal.{u, v} C)

Tactic:
rw [if_neg h]

Premises used: if_neg
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
U : (Opens (↑X : Type u))ᵒᵖ
h : p₀ ∉ unop U
⊢ IsTerminal.{u, v} (terminal.{u, v} C)

Tactic:
exact terminalIsTerminal

Premises used: CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
ℱ : Presheaf C X
x : (↑X : Type v)
⊢ obj (stalkFunctor C x) ℱ = ℱ.stalk x

Tactic:
rfl

Premises used: TopCat.Presheaf.stalk, rfl
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F : Presheaf C X
U V : Opens (↑X : Type v)
i : U ⟶ V
x : (↑X : Type v)
hx : x ∈ U
⊢ Eq (α := F.obj (op V) ⟶ F.stalk x) (F.map i.op ≫ F.germ U x hx) (F.germ V x ⋯)

Tactic:
let i' : (⟨U, hx⟩ : OpenNhds x) ⟶ ⟨V, i.le hx⟩ := i
  colimit.w ((OpenNhds.inclusion x).op ⋙ F) i'.op

Premises used: CategoryTheory.Functor.op, Set.Mem, Quiver.Hom.op, CategoryTheory.Functor.comp, TopCat.Presheaf.stalk, CategoryTheory.Limits.colimit, TopCat.Presheaf.germ, CategoryTheory.homOfLE, TopologicalSpace.OpenNhds, CategoryTheory.Limits.colimit.w, TopologicalSpace.OpenNhds.inclusion
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F : Presheaf C X
U V : Opens (↑X : Type v)
i : op V ⟶ op U
x : (↑X : Type v)
hx : x ∈ U
⊢ Eq (α := F.obj (op V) ⟶ F.stalk x) (F.map i ≫ F.germ U x hx) (F.germ V x ⋯)

Tactic:
let i' : (⟨U, hx⟩ : OpenNhds x) ⟶ ⟨V, i.unop.le hx⟩ := i.unop
  colimit.w ((OpenNhds.inclusion x).op ⋙ F) i'.op

Premises used: CategoryTheory.Functor.op, Set.Mem, Quiver.Hom.op, CategoryTheory.Functor.comp, Quiver.Hom.unop, TopCat.Presheaf.stalk, CategoryTheory.Limits.colimit, TopCat.Presheaf.germ, CategoryTheory.homOfLE, TopologicalSpace.OpenNhds, CategoryTheory.Limits.colimit.w, TopologicalSpace.OpenNhds.inclusion
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F : Presheaf C X
U : Opens (↑X : Type v)
i : U ⟶ ⊤
x : (↑X : Type v)
hx : x ∈ U
⊢ Eq (α := F.obj (op ⊤) ⟶ F.stalk x) (F.map i.op ≫ F.germ U x hx) (F.Γgerm x)

Tactic:
germ_res F i x hx

Premises used: TopCat.Presheaf.germ_res, TopCat.Presheaf.Γgerm
-- 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 u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U V : Opens (↑X : Type v)
i : U ⟶ V
x : (↑X : Type v)
hx : x ∈ U
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
s : CC (F.obj (op V))
rw :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i.op ≫ F.germ U x hx) :
          (a : CC (F.obj (op V))) → CC (F.stalk x))
        s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
rw₁ rw₂ :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i.op) : (a : CC (F.obj (op V))) → CC (F.obj (op U))) s :
          CC (F.obj (op U))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))

Tactic:
rw [← ConcreteCategory.comp_apply, germ_res]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, TopCat.Presheaf.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 u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U V : Opens (↑X : Type v)
i : op V ⟶ op U
x : (↑X : Type v)
hx : x ∈ U
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
s : CC (F.obj (op V))
rw :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i ≫ F.germ U x hx) : (a : CC (F.obj (op V))) → CC (F.stalk x))
        s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
rw₁ rw₂ :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i) : (a : CC (F.obj (op V))) → CC (F.obj (op U))) s :
          CC (F.obj (op U))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))

Tactic:
rw [← ConcreteCategory.comp_apply, 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 u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U : Opens (↑X : Type v)
i : U ⟶ ⊤
x : (↑X : Type v)
hx : x ∈ U
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
s : CC (F.obj (op ⊤))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i.op) : (a : CC (F.obj (op ⊤))) → CC (F.obj (op U))) s :
          CC (F.obj (op U))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.Γgerm x) : (a : CC (F.obj (op ⊤))) → CC (F.stalk x)) s :
      CC (F.stalk x))

Tactic:
F.germ_res_apply i x hx s

Premises used: TopCat.Presheaf.germ_res_apply, TopCat.Presheaf.Γgerm
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F : Presheaf C X
x : (↑X : Type v)
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : OpenNhds x
op :
  ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U),
    Eq (α :=
      (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F).obj
          (Opposite.op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ⟶
        Y)
      (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
          (Opposite.op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ≫
        f₁)
      (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
          (Opposite.op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ≫
        f₂)
⊢ Eq (α :=
    (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F).obj
        (Opposite.op U) ⟶
      Y)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (Opposite.op U) ≫
      f₁)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (Opposite.op U) ≫
      f₂)

Tactic:
obtain ⟨U, hxU⟩ := U
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F : Presheaf C X
x : (↑X : Type v)
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : Opens (↑X : Type v)
hxU : x ∈ U
⊢ Eq (α :=
    (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F).obj
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ⟶
      Y)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ≫
      f₁)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ≫
      f₂)

Tactic:
ih U hxU

Premises used: CategoryTheory.Functor.comp, TopCat.Presheaf.stalk, CategoryTheory.Limits.colimit, TopCat.Presheaf.germ
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F : Presheaf C X
x : (↑X : Type v)
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : Opens (↑X : Type v)
hxU : x ∈ U
⊢ Eq (α :=
    (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F).obj
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ⟶
      Y)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ≫
      f₁)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ≫
      f₂)

Tactic:
exact ih U hxU
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F : Presheaf C X
x : (↑X : Type v)
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : (OpenNhds x)ᵒᵖ
op :
  ∀ (U : OpenNhds x),
    Eq (α :=
      (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F).obj
          (Opposite.op U) ⟶
        Y)
      (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
          (Opposite.op U) ≫
        f₁)
      (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
          (Opposite.op U) ≫
        f₂)
⊢ colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F) U ≫ f₁ =
    colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F) U ≫ f₂

Tactic:
induction U with | op U => obtain ⟨U, hxU⟩ := U; exact ih U hxU

Premises used: Opposite.op
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F G : Presheaf C X
U : Opens (↑X : Type v)
x : (↑X : Type v)
hx : x ∈ U
f : F ⟶ G
⊢ Eq (α := F.obj (op U) ⟶ obj (stalkFunctor C x) G) (F.germ U x hx ≫ map (stalkFunctor C x) f)
    (f.app (op U) ≫ G.germ U x hx)

Tactic:
colimit.ι_map (whiskerLeft (OpenNhds.inclusion x).op f) (op ⟨U, hx⟩)

Premises used: CategoryTheory.Functor.op, CategoryTheory.Limits.colimit.ι_map, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, TopCat.Presheaf.stalk, CategoryTheory.Limits.colimit, Subtype.mk, TopCat.Presheaf.germ, Opposite.op, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map, TopologicalSpace.OpenNhds.inclusion
-- 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 u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F G : Presheaf C X
U : Opens (↑X : Type v)
x : (↑X : Type v)
hx : x ∈ U
f : F ⟶ G
s : CC (F.obj (op U))
rw :
  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 hx) : (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 (F.stalk x)) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s :
          CC (F.stalk x)) :
      CC (G.stalk x))
⊢ 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 hx) : (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) (G.germ U x hx) : (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))

Tactic:
rw [← ConcreteCategory.comp_apply, ← stalkFunctor_map_germ, ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, TopCat.Presheaf.stalkFunctor_map_germ