mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x✝¹ : TopologicalSpace (α × β) := lower (α × β)
b : β
x✝ : b ∈ t
⊢ (Ici (⊥, b))ᶜ = (Prod.snd ⁻¹' Ici b)ᶜ

Tactic:
simp [Ici_prod_eq, univ_prod]

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: ⊢ sierpinskiSpace = upper Prop

Tactic:
by
    rw [Topology.upper, sierpinskiSpace, ← generateFrom_insert_empty]
    congr
    exact le_antisymm
      (fun h hs => by
        simp only [compl_Iic, mem_ofPred_eq]
        rw [← Ioi_True, ← Ioi_False] at hs
        rcases hs with (rfl | rfl)
        · use True
        · use False)
      (by rintro _ ⟨a, rfl⟩; by_cases a <;> aesop (add simp [Ioi, lt_iff_le_not_ge]))

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
X✝ Y✝ : Locale
f : X✝ ⟶ Y✝
⊢ ∀ (s : Set (PT ↑(Opposite.unop Y✝))), IsOpen s → IsOpen ((fun p ↦ FrameHom.comp p (Frm.Hom.hom f.unop)) ⁻¹' s)

Tactic:
rintro s ⟨u, rfl⟩

Goal state after:
L : Type u_1
inst✝ : CompleteLattice L
X✝ Y✝ : Locale
f : X✝ ⟶ Y✝
u : ↑(Opposite.unop Y✝)
⊢ IsOpen ((fun p ↦ FrameHom.comp p (Frm.Hom.hom f.unop)) ⁻¹' {x | x u})
Module: Mathlib.Topology.Order.NhdsSet

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
⊢ (𝓝ˢ (Iic a)).HasBasis (fun x ↦ a < x) Iio

Tactic:
by
  refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨b, hab, hb⟩ ↦ mem_of_superset (Iio_mem_nhdsSet_Iic hab) hb⟩⟩
  rw [nhdsSet_Iic, mem_sup, mem_principal] at hs
  rcases exists_Ico_subset_of_mem_nhds hs.1 (Set.nonempty_coe_sort.1 h) with ⟨b, hab, hbs⟩
  exact ⟨b, hab, Iio_subset_Iio_union_Ico.trans (union_subset hs.2 hbs)⟩

Goal state after:
Module: Mathlib.Topology.Order.Priestley

Goal state before:
pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
obtain ⟨U, hU, hU', hy, hx⟩ := exists_isClopen_lower_of_not_le h

Goal state after:
case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
U : Set α
hU : IsClopen U
hU' : IsLowerSet U
hy : y ∉ U
hx : x ∈ U
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
Module: Mathlib.Topology.Order.LawsonTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsUpperSet s
⊢ IsOpen[L] s ↔ IsOpen[S] s

Tactic:
@IsLawson.topology_eq_lawson α _ L _,

Goal state after:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsUpperSet s
⊢ IsOpen[lawson α] s ↔ IsOpen[S] s
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝³ : 0 ≤ ε₂
this✝² : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝²
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝¹ : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
⊢ hausdorffDist (Fl '' univ) (Fl '' s) ≤ ε₁

Tactic:
hausdorffDist_image Il

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝³ : 0 ≤ ε₂
this✝² : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝²
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝¹ : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
⊢ hausdorffDist univ s ≤ ε₁
Module: Mathlib.Topology.Sheaves.PUnit

Goal state before:
pp: case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊥
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
⊢ x✝.Compatible → ∃! t, x✝.IsAmalgamation t

Tactic:
_

Goal state after:
case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊥
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : x✝.Compatible
⊢ ∃! t, x✝.IsAmalgamation t
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 : X
⊢ IsOpen[inst✝⁴] {y | x ≤ y}

Tactic:
IsUpperSet.isOpen_iff_isUpperSet

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 : X
⊢ IsUpperSet {y | x ≤ y}
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 : X
⊢ IsOpen[inst✝⁴] {y | x ≤ y}

Tactic:
rw [IsUpperSet.isOpen_iff_isUpperSet]

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 : X
⊢ IsUpperSet {y | x ≤ y}
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
this : IsOpen[inst✝²] ↑U
⊢ y ∈ U

Tactic:
IsUpperSet.isOpen_iff_isUpperSet

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
this : IsUpperSet ↑U
⊢ y ∈ U
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:
· simp [Presheaf.germ]
      rfl

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.LocallySurjective

Goal state before:
pp: 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 : ℱ ⟶ 𝒢
⊢ IsLocallySurjective T ↔ ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))

Tactic:
by
  constructor <;> intro hT
  · /- human proof:
        Let g ∈ Γₛₜ 𝒢 x be a germ. Represent it on an open set U ⊆ X
        as ⟨t, U⟩. By local surjectivity, pass to a smaller open set V
        on which there exists s ∈ Γ_ ℱ V mapping to t |_ V.
        Then the germ of s maps to g -/
    -- Let g ∈ Γₛₜ 𝒢 x be a germ.
    intro x g
    -- Represent it on an open set U ⊆ X as ⟨t, U⟩.
    obtain ⟨U, hxU, t, rfl⟩ := 𝒢.exists_germ_eq g
    -- By local surjectivity, pass to a smaller open set V
    -- on which there exists s ∈ Γ_ ℱ V mapping to t |_ V.
    rcases hT.imageSieve_mem t x hxU with ⟨V, ι, ⟨s, h_eq⟩, hxV⟩
    -- Then the germ of s maps to g.
    use ℱ.germ _ x hxV s
    simp [h_eq, germ_res_apply]
  · /- human proof:
        Let U be an open set, t ∈ Γ ℱ U a section, x ∈ U a point.
        By surjectivity on stalks, the germ of t is the image of
        some germ f ∈ Γₛₜ ℱ x. Represent f on some open set V ⊆ X as ⟨s, V⟩.
        Then there is some possibly smaller open set x ∈ W ⊆ V ∩ U on which
        we have T(s) |_ W = t |_ W. -/
    constructor
    intro U t x hxU
    set t_x := 𝒢.germ _ x hxU t with ht_x
    obtain ⟨s_x, hs_x : ((stalkFunctor C x).map T) s_x = t_x⟩ := hT x t_x
    obtain ⟨V, hxV, s, rfl⟩ := ℱ.exists_germ_eq s_x
    -- rfl : ℱ.germ x s = s_x
    have key_W := 𝒢.germ_eq x hxV hxU (T.app _ s) t <| by
      convert! hs_x using 1
      symm
      convert! stalkFunctor_map_germ_apply _ _ _ _ s
    obtain ⟨W, hxW, hWV, hWU, h_eq⟩ := key_W
    refine ⟨W, hWU, ⟨ℱ.map hWV.op s, ?_⟩, hxW⟩
    convert! h_eq using 1
    simp only [← ConcreteCategory.comp_apply, T.naturality]

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ↑I
⊢ range ⇑{ toFun := ⇑γ ∘ Icc.convexComb t₀ t₁, continuous_toFun := ⋯ } = range (⇑γ ∘ Icc.convexComb t₀ t₁)

Tactic:
ContinuousMap.coe_mk

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ↑I
⊢ range (⇑γ ∘ Icc.convexComb t₀ t₁) = range (⇑γ ∘ Icc.convexComb t₀ t₁)
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
⊢ IsUltraUniformity (UniformSpace.Completion X) ↔ IsUltraUniformity X

Tactic:
rw [iff_comm, ← cauchyFilter_iff, ← separationQuotient_iff]

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
⊢ IsUltraUniformity (SeparationQuotient (CauchyFilter X)) ↔ IsUltraUniformity (UniformSpace.Completion X)
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| ⨆ i, ⨆ (_ : Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
1,

Goal state after:
case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| fun i ↦ ⨆ (_ : Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x i : γ
| ⨆ (_ : Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
1,

Goal state after:
case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x i : γ
| fun x_1 ↦ comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| ⨆ i, ⨆ (_ : ¬Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
1,

Goal state after:
case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| fun i ↦ ⨆ (_ : ¬Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x i : γ
| ⨆ (_ : ¬Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
1,

Goal state after:
case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x i : γ
| fun x_1 ↦ comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i