mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∉ unop V
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj V)) =
    (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj U)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then c else ⊤_ C)

Tactic:
·

Goal state after:
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∉ unop V
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj V)) =
    (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj U)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then c else ⊤_ C)
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∈ unop U
⊢ 𝓕.germ (unop U) p₀ h ≫ fromStalk p₀ f ≫ eqToHom ⋯ = f.app U

pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∉ unop U
⊢ (⋯ ▸ terminalIsTerminal).from (𝓕.obj U) = f.app U

Tactic:
·

Goal state after:
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∈ unop U
⊢ 𝓕.germ (unop U) p₀ h ≫ fromStalk p₀ f ≫ eqToHom ⋯ = f.app U
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∉ unop U
⊢ (⋯ ▸ terminalIsTerminal).from (𝓕.obj U) = f.app U

Tactic:
·

Goal state after:
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∉ unop U
⊢ (⋯ ▸ terminalIsTerminal).from (𝓕.obj U) = f.app U
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: case mp
C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
S : ShortComplex (Sheaf C X)
⊢ S.Exact → ∀ (x : ↑X), (S.map (forget C X ⋙ stalkFunctor C x)).Exact

pp: case mpr
C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
S : ShortComplex (Sheaf C X)
⊢ (∀ (x : ↑X), (S.map (forget C X ⋙ stalkFunctor C x)).Exact) → S.Exact

Tactic:
·

Goal state after:
case mp
C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
S : ShortComplex (Sheaf C X)
⊢ S.Exact → ∀ (x : ↑X), (S.map (forget C X ⋙ stalkFunctor C x)).Exact
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
⊢ ∀ (x y : ↑(s p)), |dist x y - dist (Φ x) (Φ y)| ≤ ε

Tactic:
·

Goal state after:
case refine_3
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
⊢ ∀ (x y : ↑(s p)), |dist x y - dist (Φ x) (Φ y)| ≤ ε
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∈ U
⊢ f.app (op U) ≫ 𝓖.germ U p₀ h ≫ 𝟙 (𝓖.stalk p₀) ≫ eqToHom ⋯ =
    (𝓕.germ U p₀ h ≫ 𝟙 (𝓕.stalk p₀) ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ (Presheaf.stalkFunctor C p₀).map f ≫ eqToHom ⋯

pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∉ U
⊢ f.app (op U) ≫ (⋯ ▸ terminalIsTerminal).from (𝓖.obj (op U)) =
    (⋯ ▸ terminalIsTerminal).from (𝓕.obj (op U)) ≫ (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U then 𝓕.stalk p₀ else ⊤_ C)

Tactic:
·

Goal state after:
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∈ U
⊢ f.app (op U) ≫ 𝓖.germ U p₀ h ≫ 𝟙 (𝓖.stalk p₀) ≫ eqToHom ⋯ =
    (𝓕.germ U p₀ h ≫ 𝟙 (𝓕.stalk p₀) ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ (Presheaf.stalkFunctor C p₀).map f ≫ eqToHom ⋯
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ principalOpen x
⊢ y ∈ U

Tactic:
·

Goal state after:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ principalOpen x
⊢ y ∈ U
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∉ U
⊢ f.app (op U) ≫ (⋯ ▸ terminalIsTerminal).from (𝓖.obj (op U)) =
    (⋯ ▸ terminalIsTerminal).from (𝓕.obj (op U)) ≫ (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U then 𝓕.stalk p₀ else ⊤_ C)

Tactic:
·

Goal state after:
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∉ U
⊢ f.app (op U) ≫ (⋯ ▸ terminalIsTerminal).from (𝓖.obj (op U)) =
    (⋯ ▸ terminalIsTerminal).from (𝓕.obj (op U)) ≫ (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U then 𝓕.stalk p₀ else ⊤_ C)
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X✝ : TopCat
p₀ : ↑X✝
inst✝³ : (U : Opens ↑X✝) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
h : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j✝)
⊢ (X.germ ((OpenNhds.inclusion p₀).obj (unop j✝)) p₀ ⋯ ≫ 𝟙 (X.stalk p₀) ≫ eqToHom ⋯) ≫
      colimit.ι ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) j✝ ≫
        (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝

pp: case neg
X✝ : TopCat
p₀ : ↑X✝
inst✝³ : (U : Opens ↑X✝) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
h : p₀ ∉ (OpenNhds.inclusion p₀).obj (unop j✝)
⊢ (⋯ ▸ terminalIsTerminal).from (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j✝)))) ≫
      colimit.ι ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) j✝ ≫
        (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝

Tactic:
·

Goal state after:
case pos
X✝ : TopCat
p₀ : ↑X✝
inst✝³ : (U : Opens ↑X✝) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
h : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j✝)
⊢ (X.germ ((OpenNhds.inclusion p₀).obj (unop j✝)) p₀ ⋯ ≫ 𝟙 (X.stalk p₀) ≫ eqToHom ⋯) ≫
      colimit.ι ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) j✝ ≫
        (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case neg
X✝ : TopCat
p₀ : ↑X✝
inst✝³ : (U : Opens ↑X✝) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
h : p₀ ∉ (OpenNhds.inclusion p₀).obj (unop j✝)
⊢ (⋯ ▸ terminalIsTerminal).from (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j✝)))) ≫
      colimit.ι ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) j✝ ≫
        (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝

Tactic:
·

Goal state after:
case neg
X✝ : TopCat
p₀ : ↑X✝
inst✝³ : (U : Opens ↑X✝) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
h : p₀ ∉ (OpenNhds.inclusion p₀).obj (unop j✝)
⊢ (⋯ ▸ terminalIsTerminal).from (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j✝)))) ≫
      colimit.ι ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) j✝ ≫
        (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
Y : C
U✝ : Opens ↑X
h : p₀ ∈ U✝
⊢ ((skyscraperPresheaf p₀ Y).germ U✝ p₀ ⋯ ≫ eqToHom ⋯) ≫
      eqToHom ⋯ ≫
        (colimit.isoColimitCocone
              { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y ⋯,
                isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y ⋯ }).hom ≫
          eqToHom ⋯ =
    (𝟙 (skyscraperPresheaf p₀ Y)).app (op U✝)

pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
Y : C
U✝ : Opens ↑X
h : p₀ ∉ U✝
⊢ (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U✝ then Y else ⊤_ C) ≫
      (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U✝ then (skyscraperPresheaf p₀ Y).stalk p₀ else ⊤_ C) =
    (𝟙 (skyscraperPresheaf p₀ Y)).app (op U✝)

Tactic:
·

Goal state after:
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
Y : C
U✝ : Opens ↑X
h : p₀ ∈ U✝
⊢ ((skyscraperPresheaf p₀ Y).germ U✝ p₀ ⋯ ≫ eqToHom ⋯) ≫
      eqToHom ⋯ ≫
        (colimit.isoColimitCocone
              { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y ⋯,
                isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y ⋯ }).hom ≫
          eqToHom ⋯ =
    (𝟙 (skyscraperPresheaf p₀ Y)).app (op U✝)
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
Y : C
U✝ : Opens ↑X
h : p₀ ∉ U✝
⊢ (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U✝ then Y else ⊤_ C) ≫
      (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U✝ then (skyscraperPresheaf p₀ Y).stalk p₀ else ⊤_ C) =
    (𝟙 (skyscraperPresheaf p₀ Y)).app (op U✝)

Tactic:
·

Goal state after:
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
Y : C
U✝ : Opens ↑X
h : p₀ ∉ U✝
⊢ (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U✝ then Y else ⊤_ C) ≫
      (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U✝ then (skyscraperPresheaf p₀ Y).stalk p₀ else ⊤_ C) =
    (𝟙 (skyscraperPresheaf p₀ Y)).app (op U✝)
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
hm :
  ∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
    m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op (iSup Us))).obj left✝ ⟶ (principals ↑X).obj x
⊢ ∃ i, principalOpen x ≤ Us i

pp: X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
hm✝ :
  ∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
    m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op (iSup Us))).obj left✝ ⟶ (principals ↑X).obj x
hm :
  m ≫
      ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app
        (Opposite.op { obj := principalOpen x, property := ?m.255 }) =
    S.π.app (Opposite.op { obj := principalOpen x, property := ?m.255 })
⊢ S.π.app
        (Opposite.op
          { obj := principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }), property := ⋯ }) ≫
      limit.π (generator (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f })) ⋙ F)
        { left := { as := PUnit.unit }, right := StructuredArrow.right { left := left✝, right := x, hom := f },
          hom := 𝟙 (Opposite.op (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }))) } =
    m ≫ limit.π (generator (iSup Us) ⋙ F) { left := left✝, right := x, hom := f }

Tactic:
·

Goal state after:
X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
hm :
  ∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
    m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op (iSup Us))).obj left✝ ⟶ (principals ↑X).obj x
⊢ ∃ i, principalOpen x ≤ Us i
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
hm✝ :
  ∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
    m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op (iSup Us))).obj left✝ ⟶ (principals ↑X).obj x
hm :
  m ≫
      ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app
        (Opposite.op { obj := principalOpen x, property := ⋯ }) =
    S.π.app (Opposite.op { obj := principalOpen x, property := ⋯ })
⊢ S.π.app
        (Opposite.op
          { obj := principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }), property := ⋯ }) ≫
      limit.π (generator (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f })) ⋙ F)
        { left := { as := PUnit.unit }, right := StructuredArrow.right { left := left✝, right := x, hom := f },
          hom := 𝟙 (Opposite.op (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }))) } =
    m ≫ limit.π (generator (iSup Us) ⋙ F) { left := left✝, right := x, hom := f }

Tactic:
·

Goal state after:
X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
hm✝ :
  ∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
    m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op (iSup Us))).obj left✝ ⟶ (principals ↑X).obj x
hm :
  m ≫
      ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app
        (Opposite.op { obj := principalOpen x, property := ⋯ }) =
    S.π.app (Opposite.op { obj := principalOpen x, property := ⋯ })
⊢ S.π.app
        (Opposite.op
          { obj := principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }), property := ⋯ }) ≫
      limit.π (generator (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f })) ⋙ F)
        { left := { as := PUnit.unit }, right := StructuredArrow.right { left := left✝, right := x, hom := f },
          hom := 𝟙 (Opposite.op (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }))) } =
    m ≫ limit.π (generator (iSup Us) ⋙ F) { left := left✝, right := x, hom := f }
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
T : ℱ ⟶ 𝒢
h : IsLocallySurjective T
x✝ : Opens ↑X
t : ToType (𝒢.obj (op x✝))
x : ↑X
hx : x ∈ x✝
⊢ ∃ V, ∃ (x_1 : V ≤ x✝), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
T : ℱ ⟶ 𝒢
h :
  ∀ (U : Opens ↑X) (t : ToType (𝒢.obj (op U))),
    ∀ x ∈ U, ∃ V, ∃ (x_1 : V ≤ U), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V
U✝ : Opens ↑X
s : ToType (𝒢.obj (op U✝))
x : ↑X
hx : x ∈ U✝
⊢ ∃ U f, (Presheaf.imageSieve T s).arrows f ∧ x ∈ U

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
T : ℱ ⟶ 𝒢
h : IsLocallySurjective T
x✝ : Opens ↑X
t : ToType (𝒢.obj (op x✝))
x : ↑X
hx : x ∈ x✝
⊢ ∃ V, ∃ (x_1 : V ≤ x✝), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
T : ℱ ⟶ 𝒢
h :
  ∀ (U : Opens ↑X) (t : ToType (𝒢.obj (op U))),
    ∀ x ∈ U, ∃ V, ∃ (x_1 : V ≤ U), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V
U✝ : Opens ↑X
s : ToType (𝒢.obj (op U✝))
x : ↑X
hx : x ∈ U✝
⊢ ∃ U f, (Presheaf.imageSieve T s).arrows f ∧ x ∈ U

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
T : ℱ ⟶ 𝒢
h :
  ∀ (U : Opens ↑X) (t : ToType (𝒢.obj (op U))),
    ∀ x ∈ U, ∃ V, ∃ (x_1 : V ≤ U), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V
U✝ : Opens ↑X
s : ToType (𝒢.obj (op U✝))
x : ↑X
hx : x ∈ U✝
⊢ ∃ U f, (Presheaf.imageSieve T s).arrows f ∧ x ∈ U
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
⊢ ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))

pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
⊢ IsLocallySurjective T

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
⊢ ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))