awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (NonemptyCompacts α)
h₁ : ∀ (x : α), ∃ (i : NonemptyCompacts α), x ∈ (↑i : Set α)
⊢ Eq.{u_1 + 1} (α := Set α)
    (⋃ (K : NonemptyCompacts α), ⋃ (_ : Membership.mem (γ := Set (NonemptyCompacts α)) univ K), (↑K : Set α)) univ

Tactic:
simp_rw [biUnion_univ, eq_univ_iff_forall, mem_iUnion]

Premises used: Set.eq_univ_iff_forall, Set.mem_iUnion, Set.biUnion_univ
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (NonemptyCompacts α)
⊢ ∀ (x : α), ∃ (i : NonemptyCompacts α), x ∈ (↑i : Set α)

Tactic:
fun x => ⟨{x}, Set.mem_singleton x⟩

Premises used: Set.mem_singleton, Exists.intro, Singleton.singleton
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (NonemptyCompacts α)
⊢ ∀ (x : α), ∃ (i : NonemptyCompacts α), x ∈ (↑i : Set α)

Tactic:
exact fun x => ⟨{x}, Set.mem_singleton x⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw : ¬CompactSpace.{u_1} (NonemptyCompacts α) ↔ ¬CompactSpace α
⊢ NoncompactSpace.{u_1} (NonemptyCompacts α) ↔ NoncompactSpace α

Tactic:
simp_rw [← not_compactSpace_iff, compactSpace_iff]

Premises used: not_compactSpace_iff, TopologicalSpace.NonemptyCompacts.compactSpace_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : NoncompactSpace α
⊢ NoncompactSpace.{u_1} (NonemptyCompacts α)

Tactic:
noncompactSpace_iff.mpr ‹_›

Premises used: Iff.mpr, TopologicalSpace.NonemptyCompacts.noncompactSpace_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
⊢ LocallyCompactSpace.{u_1} (NonemptyCompacts α)

Tactic:
isOpenEmbedding_toCompacts.locallyCompactSpace

Premises used: Topology.IsOpenEmbedding.locallyCompactSpace, TopologicalSpace.NonemptyCompacts.isOpenEmbedding_toCompacts
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ LocallyCompactSpace.{u_1} (NonemptyCompacts α) ↔ LocallyCompactSpace α

Tactic:
⟨fun _ => ⟨fun x U hU => ?_⟩, fun _ => inferInstance⟩

Premises used: inferInstance, Iff.intro, LocallyCompactSpace.mk
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
refine :
  LocallyCompactSpace.{u_1} (NonemptyCompacts α) → ∀ (x : α) (U : Set α) (hU : U ∈ 𝓝 x), ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s
⊢ LocallyCompactSpace.{u_1} (NonemptyCompacts α) ↔ LocallyCompactSpace α

Tactic:
refine ⟨fun _ => ⟨fun x U hU => ?_⟩, fun _ => inferInstance⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ (↑{x} : Set α) ⊆ interior U

Tactic:
rw [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, ← coe_singleton] at hU

Premises used: Set.singleton_subset_iff, mem_interior_iff_mem_nhds, TopologicalSpace.NonemptyCompacts.coe_singleton
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
obtain :
  ∀ (K : Set (NonemptyCompacts α)) (hK : IsCompact K) (hxK : {x} ∈ interior K)
    (hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}), ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s
⊢ ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s

Tactic:
obtain ⟨K, hK, hxK, hKU⟩ := exists_compact_subset (isOpen_subsets_of_isOpen isOpen_interior) hU

Premises used: isOpen_interior, TopologicalSpace.NonemptyCompacts.isOpen_subsets_of_isOpen, exists_compact_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : {x} ∈ interior K
hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}
⊢ ∀ (i : NonemptyCompacts α) (j : i ∈ K), (↑i : Set α) ⊆ U

Tactic:
grind [interior_subset]

Premises used: interior_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : {x} ∈ interior K
hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}
refine : ⋃ L ∈ K, (↑L : Set α) ∈ 𝓝 x
⊢ ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s

Tactic:
refine ⟨⋃ L ∈ K, L, ?_, iUnion₂_subset <| by grind [interior_subset],
    isCompact_biUnion_coe_of_isCompact hK⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : {x} ∈ interior K
hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}
⊢ Membership.mem (γ := Filter (NonemptyCompacts α)) (𝓝 {x}) K

Tactic:
rw [mem_interior_iff_mem_nhds] at hxK

Premises used: mem_interior_iff_mem_nhds
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : {x} ∈ interior K
hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}
hxK₁ : Membership.mem (γ := Filter (NonemptyCompacts α)) (𝓝 {x}) K
⊢ K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}

Tactic:
rw [mem_interior_iff_mem_nhds] at hxK

Premises used: mem_interior_iff_mem_nhds
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : Membership.mem (γ := Filter (NonemptyCompacts α)) (𝓝 {x}) K
hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}
y : α
hy : Membership.mem (γ := Set α) ((fun (x : α) ↦ {x}) ⁻¹' K) y
⊢ Membership.mem (γ := Set α) (⋃ L ∈ K, (↑L : Set α)) y

Tactic:
mem_iUnion₂_of_mem hy rfl

Premises used: Set.mem_iUnion₂_of_mem, rfl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h_1 : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : Membership.mem (γ := Filter (NonemptyCompacts α)) (𝓝 {x}) K
hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) ((fun (x : α) ↦ {x}) ⁻¹' K) x →
          Membership.mem (γ := Set α) (⋃ L ∈ K, (↑L : Set α)) x}
      a
h₁ h₂ :
  ∀ (y : α) (hy : Membership.mem (γ := Set α) ((fun (x : α) ↦ {x}) ⁻¹' K) y),
    Membership.mem (γ := Set α) (⋃ L ∈ K, (↑L : Set α)) y
⊢ ⋃ L ∈ K, (↑L : Set α) ∈ 𝓝 x

Tactic:
filter_upwards [continuous_singleton.tendsto x hxK] with y hy using mem_iUnion₂_of_mem hy rfl

Premises used: Continuous.tendsto, TopologicalSpace.NonemptyCompacts.continuous_singleton
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ LocallyCompactSpace.{u_1} (Compacts α) ↔ LocallyCompactSpace α

Tactic:
⟨fun _ => NonemptyCompacts.locallyCompactSpace_iff.mp
    isOpenEmbedding_toCompacts.locallyCompactSpace, fun _ => inferInstance⟩

Premises used: TopologicalSpace.NonemptyCompacts.locallyCompactSpace_iff, inferInstance, Topology.IsOpenEmbedding.locallyCompactSpace, TopologicalSpace.NonemptyCompacts.isOpenEmbedding_toCompacts, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
X : TopCat
C : Type v₁
inst : Category.{v₂, v₁} C
inst_1 : HasSheafify.{u, v₂, u, v₁} (C := Opens (↑X : Type u)) (Opens.grothendieckTopology (↑X : Type u)) C
inst_2 : Abelian.{v₂, v₁} C
D : Type u_1
inst_3 : Category.{u, u_1} D
inst_4 : Abelian.{u, u_1} D
inst_5 : IsGrothendieckAbelian.{u, u, u_1} D
inst_6 : HasSheafify.{u, u, u, u_1} (C := Opens (↑X : Type u)) (Opens.grothendieckTopology (↑X : Type u)) D
⊢ IsGrothendieckAbelian.{u, u, max u_1 u} (Sheaf D X)

Tactic:
inferInstanceAs (IsGrothendieckAbelian (CategoryTheory.Sheaf _ _))

Premises used: _private.0.TopCat.Sheaf.instIsGrothendieckAbelian._proof_1
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
X : TopCat
p₀ : (↑X : Type u)
C : Type v
inst : Category.{u, v} C
inst_1 : Abelian.{u, v} C
inst_2 : HasColimits.{u, v} C
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X_1 Y : CategoryTheory.Functor.{u, u, u, v} (Opens (↑X : Type u))ᵒᵖ C} {f g : X_1 ⟶ Y},
    CategoryTheory.Functor.map
        (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op)
        (f + g) =
      HAdd.hAdd (α :=
        Functor.obj
            (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op)
            X_1 ⟶
          Functor.obj
            (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op)
            Y)
        (CategoryTheory.Functor.map
          (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op) f)
        (CategoryTheory.Functor.map
          (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op) g)
⊢ ∀ {X_1 Y : CategoryTheory.Functor.{u, u, u, v} (Opens (↑X : Type u))ᵒᵖ C} {f g : X_1 ⟶ Y},
    CategoryTheory.Functor.map
        (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op)
        (f + g) =
      HAdd.hAdd (α :=
        Functor.obj
            (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op)
            X_1 ⟶
          Functor.obj
            (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op)
            Y)
        (CategoryTheory.Functor.map
          (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op) f)
        (CategoryTheory.Functor.map
          (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op) g)

Tactic:
cat_disch
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
X : TopCat
p₀ : (↑X : Type u)
C : Type v
inst : Category.{u, v} C
inst_1 : Abelian.{u, v} C
inst_2 : HasColimits.{u, v} C
⊢ Functor.Additive (C := CategoryTheory.Functor.{u, u, u, v} (Opens (↑X : Type u))ᵒᵖ C)
    (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op)

Tactic:
have : ((Functor.whiskeringLeft _ _ C).obj (OpenNhds.inclusion p₀).op).Additive := ⟨by cat_disch⟩
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
X : TopCat
p₀ : (↑X : Type u)
C : Type v
inst : Category.{u, v} C
inst_1 : Abelian.{u, v} C
inst_2 : HasColimits.{u, v} C
this :
  Functor.Additive (C := CategoryTheory.Functor.{u, u, u, v} (Opens (↑X : Type u))ᵒᵖ C)
    (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op)
⊢ Functor.Additive (C := Presheaf C X)
    (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op ⋙ colim)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
X_1 : TopCat
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
p₀ : (↑X : Type u)
S : ShortComplex (Sheaf C X)
h : S.ShortExact
⊢ ∀ (S : ShortComplex (Sheaf C X)),
    S.ShortExact →
      ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C p₀)) ∧
        Epi (X := Functor.obj (forget C X ⋙ stalkFunctor C p₀) S.X₂)
          (CategoryTheory.Functor.map (forget C X ⋙ stalkFunctor C p₀) S.g)

Tactic:
have := ((forget C X ⋙ stalkFunctor C p₀).preservesFiniteColimits_tfae.out 3 0).mp
      (inferInstance : (PreservesFiniteColimits _))
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
X_1 : TopCat
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
p₀ : (↑X : Type u)
S : ShortComplex (Sheaf C X)
h : S.ShortExact
this :
  ∀ (S : ShortComplex (Sheaf C X)),
    S.ShortExact →
      ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C p₀)) ∧
        Epi (X := Functor.obj (forget C X ⋙ stalkFunctor C p₀) S.X₂)
          (CategoryTheory.Functor.map (forget C X ⋙ stalkFunctor C p₀) S.g)
⊢ ShortComplex.ShortExact (S.map (forget C X ⋙ stalkFunctor C p₀))

Tactic:
ShortComplex.ShortExact.mk' (this S h).left ?_ (this S h).right

Premises used: CategoryTheory.ShortComplex.ShortExact.mk', And.right, And.left
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
X_1 : TopCat
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
p₀ : (↑X : Type u)
S : ShortComplex (Sheaf C X)
h : S.ShortExact
this :
  ∀ (S : ShortComplex (Sheaf C X)),
    S.ShortExact →
      ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C p₀)) ∧
        Epi (X := Functor.obj (forget C X ⋙ stalkFunctor C p₀) S.X₂)
          (CategoryTheory.Functor.map (forget C X ⋙ stalkFunctor C p₀) S.g)
refine :
  Mono (X := ShortComplex.X₁ (S.map (forget C X ⋙ stalkFunctor C p₀)))
    (ShortComplex.f (S.map (forget C X ⋙ stalkFunctor C p₀)))
⊢ ShortComplex.ShortExact (S.map (forget C X ⋙ stalkFunctor C p₀))

Tactic:
refine ShortComplex.ShortExact.mk' (this S h).left ?_ (this S h).right

Premises used: CategoryTheory.ShortComplex.ShortExact.mk', And.right, And.left
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
X_1 : TopCat
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
p₀ : (↑X : Type u)
S : ShortComplex (Sheaf C X)
h : S.ShortExact
this :
  ∀ (S : ShortComplex (Sheaf C X)),
    S.ShortExact →
      ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C p₀)) ∧
        Epi (X := Functor.obj (forget C X ⋙ stalkFunctor C p₀) S.X₂)
          (CategoryTheory.Functor.map (forget C X ⋙ stalkFunctor C p₀) S.g)
⊢ Mono S.f

Tactic:
have := h.2
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
X_1 : TopCat
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
p₀ : (↑X : Type u)
S : ShortComplex (Sheaf C X)
h : S.ShortExact
this_1 :
  ∀ (S : ShortComplex (Sheaf C X)),
    S.ShortExact →
      ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C p₀)) ∧
        Epi (X := Functor.obj (forget C X ⋙ stalkFunctor C p₀) S.X₂)
          (CategoryTheory.Functor.map (forget C X ⋙ stalkFunctor C p₀) S.g)
this : Mono S.f
⊢ Mono (X := ShortComplex.X₁ (S.map (forget C X ⋙ stalkFunctor C p₀)))
    (ShortComplex.f (S.map (forget C X ⋙ stalkFunctor C p₀)))

Tactic:
Functor.map_mono (forget C X ⋙ stalkFunctor C p₀) _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.map_mono, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map, TopCat.Presheaf.stalkFunctor, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
X_1 : TopCat
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
p₀ : (↑X : Type u)
S : ShortComplex (Sheaf C X)
h : S.ShortExact
this_1 :
  ∀ (S : ShortComplex (Sheaf C X)),
    S.ShortExact →
      ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C p₀)) ∧
        Epi (X := Functor.obj (forget C X ⋙ stalkFunctor C p₀) S.X₂)
          (CategoryTheory.Functor.map (forget C X ⋙ stalkFunctor C p₀) S.g)
this : Mono S.f
⊢ Mono (X := ShortComplex.X₁ (S.map (forget C X ⋙ stalkFunctor C p₀)))
    (ShortComplex.f (S.map (forget C X ⋙ stalkFunctor C p₀)))

Tactic:
exact Functor.map_mono (forget C X ⋙ stalkFunctor C p₀) _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.map_mono, TopCat.Presheaf.stalkFunctor, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
F : Sheaf C X
⊢ IsZero F ↔ ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)

Tactic:
⟨fun h _ => Functor.map_isZero _ h, ?_⟩

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.map_isZero, Iff.intro, TopCat.Presheaf.stalkFunctor, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
F : Sheaf C X
refine : (∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)) → IsZero F
⊢ IsZero F ↔ ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)

Tactic:
refine ⟨fun h _ => Functor.map_isZero _ h, ?_⟩
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
F : Sheaf C X
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)
f : F ⟶ 0 := IsZero.from_ ⋯ F
rw :
  ∀ (x : (↑X : Type u)),
    IsIso (X :=
      Functor.obj (stalkFunctor C x)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u)))))
      (CategoryTheory.Functor.map (stalkFunctor C x) f.hom)
⊢ IsIso f

Tactic:
rw [Presheaf.isIso_iff_stalkFunctor_map_iso]

Premises used: TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
F : Sheaf C X
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)
f : F ⟶ 0 := IsZero.from_ ⋯ F
⊢ ∀ (x : (↑X : Type u)),
    IsIso (X :=
      Functor.obj (stalkFunctor C x)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u)))))
      (CategoryTheory.Functor.map (stalkFunctor C x) f.hom)

Tactic:
fun x => isIso_of_source_target_iso_zero _ (h x).isoZero
      ((forget C X ⋙ stalkFunctor C x).map_isZero (isZero_zero _)).isoZero

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Functor.comp, CategoryTheory.Functor.map_isZero, TopCat.Sheaf, CategoryTheory.Functor.map, CategoryTheory.Limits.isIso_of_source_target_iso_zero, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Limits.IsZero.isoZero, TopCat.Presheaf.stalkFunctor, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
F : Sheaf C X
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)
f : F ⟶ 0 := IsZero.from_ ⋯ F
⊢ ∀ (x : (↑X : Type u)),
    IsIso (X :=
      Functor.obj (stalkFunctor C x)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u)))))
      (CategoryTheory.Functor.map (stalkFunctor C x) f.hom)

Tactic:
exact fun x => isIso_of_source_target_iso_zero _ (h x).isoZero
      ((forget C X ⋙ stalkFunctor C x).map_isZero (isZero_zero _)).isoZero

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Functor.comp, CategoryTheory.Functor.map_isZero, TopCat.Sheaf, CategoryTheory.Limits.isIso_of_source_target_iso_zero, CategoryTheory.Limits.IsZero.isoZero, TopCat.Presheaf.stalkFunctor, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Abelian
Goal:
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
F : Sheaf C X
h : ∀ (x : (↑X : Type u)), IsZero.{u, v} (Functor.obj (forget C X ⋙ stalkFunctor C x) F)
f : F ⟶ 0 := IsZero.from_ ⋯ F
⊢ IsIso f

Tactic:
have : IsIso f := by
    rw [Presheaf.isIso_iff_stalkFunctor_map_iso]
    exact fun x => isIso_of_source_target_iso_zero _ (h x).isoZero
      ((forget C X ⋙ stalkFunctor C x).map_isZero (isZero_zero _)).isoZero