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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : (𝓝[>] a).NeBot
⊢ (𝓝ˢ (Iic a)).HasBasis (fun x ↦ a < x) Iic

Tactic:
have : Nonempty (Ioi a) :=
    (Filter.nonempty_of_mem (self_mem_nhdsWithin : Ioi a ∈ 𝓝[>] a)).to_subtype

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : (𝓝[>] a).NeBot
this : Nonempty ↑(Ioi a)
⊢ (𝓝ˢ (Iic a)).HasBasis (fun x ↦ a < x) Iic
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case h₂
x : GHSpace
y : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ 0 ∈ (fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = x}

Tactic:
simp only [mem_image, mem_prod, mem_ofPred_eq, Prod.exists]

Goal state after:
case h₂
x : GHSpace
y : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ ∃ a b, (⟦a⟧ = x ∧ ⟦b⟧ = x) ∧ hausdorffDist ↑a ↑b = 0
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case right
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)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fr '' range Φ
y : Y
y_in_s' : y ∈ range Φ
yx' : Fr y = x'
x : ↑s
xy : Φ x = y
⊢ dist (Fr (Φ x)) (Fl ↑x) ≤ ε₂ / 2 + δ

Tactic:
dist_comm

Goal state after:
case right
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)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fr '' range Φ
y : Y
y_in_s' : y ∈ range Φ
yx' : Fr y = x'
x : ↑s
xy : Φ x = y
⊢ dist (Fl ↑x) (Fr (Φ x)) ≤ ε₂ / 2 + δ
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s t : Set X
hs : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
g : C(X, ℝ)
hg : t = ⇑g ⁻¹' {0}
hgr : ∀ (x : X), g x ∈ Icc 0 1
hsn : SeparatedNhds {0} {1}
⊢ SeparatedNhds s t

Tactic:
have hfg (x : X) : f x + g x ≠ 0 := by
          simp_all only [preimage, mem_singleton_iff]
          by_cases! hfx : f x = 0
          · simpa [hfx] using hst.notMem_of_mem_left hfx
          · positivity [(hgr x).1, (hfr x).1]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s t : Set X
hs : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
g : C(X, ℝ)
hg : t = ⇑g ⁻¹' {0}
hgr : ∀ (x : X), g x ∈ Icc 0 1
hsn : SeparatedNhds {0} {1}
hfg : ∀ (x : X), f x + g x ≠ 0
⊢ SeparatedNhds s t
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case hc
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U)))

Tactic:
· exact h.mem_open U.unop.1.2 U.unop.2

Goal state after:
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:
exact ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext ..

Goal state after:
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)
h : S.Exact
x : ↑X
⊢ (S.map (forget C X ⋙ stalkFunctor C x)).Exact

Tactic:
have := (forget C X ⋙ stalkFunctor C x).exact_tfae.out 2 1

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)
h : S.Exact
x : ↑X
this :
  (forget C X ⋙ stalkFunctor C x).PreservesHomology ↔
    ∀ (S : ShortComplex (Sheaf C X)), S.Exact → (S.map (forget C X ⋙ stalkFunctor C x)).Exact
⊢ (S.map (forget C X ⋙ stalkFunctor C x)).Exact
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
ι : Type v
x : X
Us : ι → Opens X
h : principalOpen x ≤ iSup Us
⊢ ∃ i, principalOpen x ≤ Us i

Tactic:
grind [principalOpen_le_iff, Opens.mem_iSup]

Goal state after:
Module: Mathlib.Topology.Sheaves.MayerVietoris

Goal state before:
pp: case inl
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₂
⊢ ∃ U f, (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

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

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case neg
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
p : GHSpace
hp : ¬p ∉ t
s : Set p.Rep
scover : univ ⊆ ⋃ x ∈ s, ball x (u n)
N : ℕ
scard : N ≤ K n
hN : #↑s = ↑N
this : #↑s = #(Fin N)
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)

Tactic:
obtain ⟨E⟩ := Quotient.exact this

Goal state after:
case neg
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
p : GHSpace
hp : ¬p ∉ t
s : Set p.Rep
scover : univ ⊆ ⋃ x ∈ s, ball x (u n)
N : ℕ
scard : N ≤ K n
hN : #↑s = ↑N
this : #↑s = #(Fin N)
E : ↑s ≃ Fin N
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
⊢ ∃ ub, ∀ a ∈ c, Nonempty (ub ⟶ a)

Tactic:
obtain ⟨t, ht, _⟩ : ∃! s_1, IsGluing F.obj f (fun x => x.val.right.2) s_1 := by
    refine Sheaf.existsUnique_gluing F _ _ (fun i j ↦ ?_)
    obtain (rfl | h₁ | h₁) : i = j ∨ Nonempty (i.val ⟶ j.val) ∨ Nonempty (j.val ⟶ i.val) := by
      grind [Subtype.ext_iff, h i.property j.property]
    · rfl
    all_goals
      rw [← CategoryOfElements.map_snd h₁.some.2]
      dsimp
      rw [← Functor.map_comp_apply]
      rfl

Goal state after:
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
t : ToType (F.obj.obj (op (iSup f)))
ht : IsGluing F.obj f (fun x ↦ (StructuredArrow.right ↑x).snd) t
right✝ :
  ∀ (y : ToType (F.obj.obj (op (iSup f)))),
    (fun s_1 ↦ IsGluing F.obj f (fun x ↦ (StructuredArrow.right ↑x).snd) s_1) y → y = t
⊢ ∃ ub, ∀ a ∈ c, Nonempty (ub ⟶ a)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r
z : Y
I1 : ⨆ y, ⨅ x, (optimalGHDist X Y) (inl x, inr y) < r
I2 : ⨅ x, (optimalGHDist X Y) (inl x, inr z) ≤ ⨆ y, ⨅ x, (optimalGHDist X Y) (inl x, inr y)
I : ⨅ x, (optimalGHDist X Y) (inl x, inr z) < r
z' : X
hr' : (fun x ↦ (optimalGHDist X Y) (inl x, inr z)) z' < r
⊢ dist (optimalGHInjr X Y z) (optimalGHInjl X Y z') < r

Tactic:
dist_comm

Goal state after:
case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r
z : Y
I1 : ⨆ y, ⨅ x, (optimalGHDist X Y) (inl x, inr y) < r
I2 : ⨅ x, (optimalGHDist X Y) (inl x, inr z) ≤ ⨆ y, ⨅ x, (optimalGHDist X Y) (inl x, inr y)
I : ⨅ x, (optimalGHDist X Y) (inl x, inr z) < r
z' : X
hr' : (fun x ↦ (optimalGHDist X Y) (inl x, inr z)) z' < r
⊢ dist (optimalGHInjl X Y z') (optimalGHInjr X Y z) < r
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
⊢ CompactSpace X

Tactic:
apply compactSpace_generateFrom_of_compl_mem (T := constructibleTopology X) 𝔅 rfl (by simp [𝔅])

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := ⋯
⊢ ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
Module: Mathlib.Topology.UniformSpace.Dini

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
⊢ TendstoLocallyUniformly F f atTop

Tactic:
simp_rw [Metric.tendstoLocallyUniformly_iff, dist_eq_norm']

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
⊢ ∀ ε > 0, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
⊢ (∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 X, ball x V ⊆ s

Tactic:
· rintro ⟨V, V_in, _, _, V_sub⟩
    exact ⟨V, V_in, V_sub⟩

Goal state after:
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
⊢ (𝓝Δ.lift' fun s ↦ s ○ s) ≤ 𝓝Δ

Tactic:
set F := 𝓝Δ.lift' fun s : Set (γ × γ) => s ○ s

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun s ↦ s ○ s
⊢ F ≤ 𝓝Δ