awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
W : Opens (↑X : Type v)
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))
mpr :
  Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op W)) : (a : CC (ℱ.obj (op W))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.map hWV.op) : (a : CC (ℱ.obj (op V))) → CC (ℱ.obj (op W))) s :
          CC (ℱ.obj (op W))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1

Tactic:
refine ⟨W, hWU, ⟨ℱ.map hWV.op s, ?_⟩, hxW⟩
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
W : Opens (↑X : Type v)
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))
⊢ Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))

Tactic:
h_eq
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
W : Opens (↑X : Type v)
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))
h :
  Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op W)) : (a : CC (ℱ.obj (op W))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.map hWV.op) : (a : CC (ℱ.obj (op V))) → CC (ℱ.obj (op W))) s :
          CC (ℱ.obj (op W))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.obj (op W)))
⊢ Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op W)) : (a : CC (ℱ.obj (op W))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.map hWV.op) : (a : CC (ℱ.obj (op V))) → CC (ℱ.obj (op W))) s :
          CC (ℱ.obj (op W))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))

Tactic:
convert! h_eq using 1
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_x :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) =
    t_x
W : Opens (↑X : Type v)
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))
⊢ Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op W)) : (a : CC (ℱ.obj (op W))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.map hWV.op) : (a : CC (ℱ.obj (op V))) → CC (ℱ.obj (op W))) s :
          CC (ℱ.obj (op W))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.obj (op W)))

Tactic:
simp only [← ConcreteCategory.comp_apply, T.naturality]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Topology.Sheaves.LocallySurjective
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 :
  Balanced (CategoryTheory.Sheaf.{v, v, v, u} (C := Opens (↑X : Type v)) (Opens.grothendieckTopology (↑X : Type v)) C)
inst_4 :
  GrothendieckTopology.HasSheafCompose (C := Opens (↑X : Type v)) (Opens.grothendieckTopology (↑X : Type v))
    (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : HasSheafify.{v, v, v, u} (C := Opens (↑X : Type v)) (Opens.grothendieckTopology (↑X : Type v)) C
inst_6 :
  GrothendieckTopology.WEqualsLocallyBijective (C := Opens (↑X : Type v)) (Opens.grothendieckTopology (↑X : Type v)) C
    (FA := FC) (CA := CC)
inst_7 : ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization C (FC := FC) (CC := CC)
F G : Sheaf C X
φ : F ⟶ G
⊢ Presheaf.IsLocallySurjective (FC := FC) (CC := CC) φ.hom ↔ Epi φ

Tactic:
CategoryTheory.Sheaf.isLocallySurjective_iff_epi' ..

Premises used: CategoryTheory.Sheaf.isLocallySurjective_iff_epi', TopCat.Sheaf, TopCat.Presheaf.IsLocallySurjective
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
refine_1 : (s : PullbackCone sq.f₂₄ sq.f₃₄) → s.pt ⟶ sq.X₁
refine_2 : ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄), homOfLE ⋯ ≫ sq.f₁₂ = s.fst
refine_3 : ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄), homOfLE ⋯ ≫ sq.f₁₃ = s.snd
refine_4 :
  ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄) (m : s.pt ⟶ sq.X₁), m ≫ sq.f₁₂ = s.fst → m ≫ sq.f₁₃ = s.snd → m = homOfLE ⋯
⊢ IsLimit sq.pullbackCone

Tactic:
refine PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.mk
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
refine_1 : s.pt ≤ sq.X₁
⊢ s.pt ⟶ sq.X₁

Tactic:
apply homOfLE

Premises used: CategoryTheory.homOfLE
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
refine_1 : s.pt ≤ sq.X₂ ∧ s.pt ≤ sq.X₃
⊢ s.pt ≤ sq.X₁

Tactic:
rw [h₁, le_inf_iff]

Premises used: le_inf_iff
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
⊢ s.pt ≤ sq.X₂ ∧ s.pt ≤ sq.X₃

Tactic:
⟨leOfHom s.fst, leOfHom s.snd⟩

Premises used: CategoryTheory.Limits.PullbackCone.fst, And.intro, CategoryTheory.Limits.PullbackCone.snd, CategoryTheory.leOfHom
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
⊢ s.pt ≤ sq.X₂ ∧ s.pt ≤ sq.X₃

Tactic:
exact ⟨leOfHom s.fst, leOfHom s.snd⟩
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
⊢ homOfLE ⋯ ≫ sq.f₁₂ = s.fst

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
⊢ homOfLE ⋯ ≫ sq.f₁₃ = s.snd

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
m : s.pt ⟶ sq.X₁
h : m ≫ sq.f₁₂ = s.fst
h_1 : m ≫ sq.f₁₃ = s.snd
⊢ m = homOfLE ⋯

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ sq.X₄
⊢ x ∈ sq.X₂ ⊔ sq.X₃

Tactic:
rw [h₄] at hx
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ sq.X₂ ⊔ sq.X₃
inl : ∀ (hx : x ∈ (↑sq.X₂ : Set T)), ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U
inr : ∀ (hx : x ∈ (↑sq.X₃ : Set T)), ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

Tactic:
obtain (hx | hx) := hx
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ (↑sq.X₂ : Set T)
⊢ ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

Tactic:
⟨_, _, ⟨Sieve.ofArrows_mk _ _ WalkingPair.left, hx⟩⟩

Premises used: CategoryTheory.Sieve.ofArrows_mk, And.intro, Exists.intro, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ (↑sq.X₂ : Set T)
⊢ ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

Tactic:
exact ⟨_, _, ⟨Sieve.ofArrows_mk _ _ WalkingPair.left, hx⟩⟩
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ (↑sq.X₃ : Set T)
⊢ ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

Tactic:
⟨_, _, ⟨Sieve.ofArrows_mk _ _ WalkingPair.right, hx⟩⟩

Premises used: CategoryTheory.Sieve.ofArrows_mk, CategoryTheory.Limits.WalkingPair.right, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sheaves.MayerVietoris
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ (↑sq.X₃ : Set T)
⊢ ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

Tactic:
exact ⟨_, _, ⟨Sieve.ofArrows_mk _ _ WalkingPair.right, hx⟩⟩
-- Module: Mathlib.Topology.Sheaves.Over
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
W : Opens ↥U
x : X
h : x ∈ { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) '' (↑W : Set ↥U), is_open' := ⋯ : Opens X }
⊢ x ∈ U

Tactic:
aesop
-- Module: Mathlib.Topology.Sheaves.Over
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
V : Over U
h :
  ∀ (x : X),
    x ∈ (↑(Functor.obj (𝟭 (Over U)) V).left : Set X) ↔
      x ∈
        (↑(Over.left (X := U)
              (Functor.obj
                (Functor.comp (D := Opens ↥U)
                  {
                    obj := fun (V : Over U) ↦
                      { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' (↑V.left : Set X), is_open' := ⋯ :
                        Opens ↥U },
                    map := fun {X_1 Y : Over U} (f : X_1 ⟶ Y) ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ :
                    Over U ⥤ Opens ↥U }
                  {
                    obj := fun (W : Opens ↥U) ↦
                      Over.mk (Y :=
                        { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) '' (↑W : Set ↥U), is_open' := ⋯ : Opens X })
                        (homOfLE ⋯),
                    map := fun {X_1 Y : Opens ↥U} (f : X_1 ⟶ Y) ↦ Over.homMk (homOfLE ⋯) ⋯, map_id := ⋯, map_comp := ⋯ :
                    Opens ↥U ⥤ Over U })
                V)) :
          Set X)
⊢ (Functor.obj (𝟭 (Over U)) V).left =
    Over.left (X := U)
      (Functor.obj
        (Functor.comp (D := Opens ↥U)
          {
            obj := fun (V : Over U) ↦
              { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' (↑V.left : Set X), is_open' := ⋯ },
            map := fun {X_1 Y : Over U} (f : X_1 ⟶ Y) ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
          {
            obj := fun (W : Opens ↥U) ↦
              Over.mk (Y := { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) '' (↑W : Set ↥U), is_open' := ⋯ })
                (homOfLE ⋯),
            map := fun {X_1 Y : Opens ↥U} (f : X_1 ⟶ Y) ↦ Over.homMk (homOfLE ⋯) ⋯, map_id := ⋯, map_comp := ⋯ })
        V)

Tactic:
ext x
-- Module: Mathlib.Topology.Sheaves.Over
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
V : Over U
x : X
h :
  x ∈ (↑V.left : Set X) ↔
    x ∈
      Set.image (α := ↥U) (Subtype.val (p := fun (x : X) ↦ x ∈ U))
        (Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' (↑V.left : Set X))
⊢ x ∈ (↑(Functor.obj (𝟭 (Over U)) V).left : Set X) ↔
    x ∈
      (↑(Over.left (X := U)
            (Functor.obj
              (Functor.comp (D := Opens ↥U)
                {
                  obj := fun (V : Over U) ↦
                    { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' (↑V.left : Set X), is_open' := ⋯ :
                      Opens ↥U },
                  map := fun {X_1 Y : Over U} (f : X_1 ⟶ Y) ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ :
                  Over U ⥤ Opens ↥U }
                {
                  obj := fun (W : Opens ↥U) ↦
                    Over.mk (Y :=
                      { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) '' (↑W : Set ↥U), is_open' := ⋯ : Opens X })
                      (homOfLE ⋯),
                  map := fun {X_1 Y : Opens ↥U} (f : X_1 ⟶ Y) ↦ Over.homMk (homOfLE ⋯) ⋯, map_id := ⋯, map_comp := ⋯ :
                  Opens ↥U ⥤ Over U })
              V)) :
        Set X)

Tactic:
dsimp
-- Module: Mathlib.Topology.Sheaves.Over
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
V : Over U
x : X
h : x ∈ V.left → x ∈ U
⊢ x ∈ (↑V.left : Set X) ↔
    x ∈
      Set.image (α := ↥U) (Subtype.val (p := fun (x : X) ↦ x ∈ U))
        (Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' (↑V.left : Set X))

Tactic:
simp only [SetLike.mem_coe, Set.mem_image, Set.mem_preimage,
      Subtype.exists, exists_and_left, exists_prop, exists_eq_right_right, iff_self_and]

Premises used: exists_eq_right_right, Set.mem_image, Subtype.exists, iff_self_and, exists_and_left, exists_prop, SetLike.mem_coe, Set.mem_preimage
-- Module: Mathlib.Topology.Sheaves.Over
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
V : Over U
x : X
⊢ x ∈ V.left → x ∈ U

Tactic:
apply leOfHom V.hom

Premises used: CategoryTheory.leOfHom, CategoryTheory.Over.hom
-- Module: Mathlib.Topology.Sheaves.Over
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
V : Opens ↥U
⊢ Functor.obj
      (Functor.comp (D := Over U)
        {
          obj := fun (W : Opens ↥U) ↦
            Over.mk (Y := { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) '' (↑W : Set ↥U), is_open' := ⋯ })
              (homOfLE ⋯),
          map := fun {X_1 Y : Opens ↥U} (f : X_1 ⟶ Y) ↦ Over.homMk (homOfLE ⋯) ⋯, map_id := ⋯, map_comp := ⋯ }
        {
          obj := fun (V : Over U) ↦
            { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' (↑V.left : Set X), is_open' := ⋯ },
          map := fun {X_1 Y : Over U} (f : X_1 ⟶ Y) ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ })
      V =
    Functor.obj (𝟭 (Opens ↥U)) V

Tactic:
aesop
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
⊢ IndiscreteTopology.{w} (↑X : Type w)

Tactic:
have : IndiscreteTopology X := ⟨hind⟩
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this : IndiscreteTopology.{w} (↑X : Type w)
inl :
  ∀ (s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥)
    (hs :
      Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
        ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s),
    Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (op c)) s.arrows
inr : ∀ (hne : U ≠ ⊥), Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (op c)) s.arrows
⊢ Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (op c)) s.arrows

Tactic:
obtain rfl | hne := eq_or_ne U ⊥

Premises used: Bot.bot, eq_or_ne, rfl