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

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ ((⨅ i ∈ I, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (eval i) (𝓝 (x i)) =
    (⨅ i ∈ I, comap (fun x ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x ↦ x i) ⁻¹' s i)) ⊓
      ⨅ i, ⨅ (_ : i ∉ I), comap (fun x ↦ x i) (𝓝 (x i))

Tactic:
simp only [iInf_inf_eq]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ (∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s) →
    ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)

Tactic:
intro h t ht

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen[inst✝] t
⊢ IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ (∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)) →
    ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
intro h t ht

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen[inst✝] t
⊢ ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen[inst✝¹] s
hp : f ⁻¹' t ⊆ s
ht : IsOpen[inst✝] t
⊢ f ⁻¹' t = s ∩ f ⁻¹' t

Tactic:
rw [inter_comm, inter_eq_self_of_subset_left hp]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
h : IsClosed[inst✝] {a | p a}
⊢ IsClosed[inst✝] (range Subtype.val)

Tactic:
by rwa [Subtype.range_coe_subtype]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
⊢ IsOpenMap f ↔ ∀ s ∈ B, IsOpen[inst✝] (f '' s)

Tactic:
refine ⟨fun H o ho => H _ (hB.isOpen ho), fun hf o ho => ?_⟩

Goal state after:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen[inst✝] (f '' s)
o : Set α
ho : IsOpen[t] o
⊢ IsOpen[inst✝] (f '' o)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ⋃₀ ∅ = univ

Tactic:
by simp [Set.univ_eq_empty_iff.2]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ⋃₀ {∅} = univ

Tactic:
by simp [Set.univ_eq_empty_iff.2]

Goal state after:
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
⊢ IsBounded (f '' s)

Tactic:
obtain ⟨t, ht, hts⟩ := h hs.compl

Goal state after:
α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : f ⁻¹' t ⊆ sᶜ
⊢ IsBounded (f '' s)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2.refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
⊢ ((↑I).pi fun a ↦ if a ∈ I then t a else univ) ⊆ s

Tactic:
rw [← univ_pi_ite]
      simp only [← ite_and, ← Finset.mem_coe, and_self_iff, univ_pi_ite, h2]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
⊢ ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i

Tactic:
simp_rw [← Subtype.exists_set_subtype, biUnion_image]
  rcases isOpen_iUnion_countable (fun i : I ↦ s i) fun i ↦ H i i.2 with ⟨T, hTc, hU⟩
  exact ⟨T, hTc.image _, hU.trans <| iUnion_subtype ..⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
⊢ ∃ v_1, (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v

Tactic:
obtain ⟨u, u_mem, xu, uv⟩ : ∃ u ∈ countableBasis α, x ∈ u ∧ u ⊆ v :=
      (isBasis_countableBasis α).isOpen_iff.1 hv _ hx

Goal state after:
case h_nhds
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
⊢ ∃ v_1, (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst✝] (t i)
i₀ : ι := hι.some
this : (t i₀ ∩ ⋂ i, t i).Nonempty
⊢ (⋂ i, t i).Nonempty

Tactic:
inter_eq_right.mpr (iInter_subset _ i₀)

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst✝] (t i)
i₀ : ι := hι.some
this : (⋂ i, t i).Nonempty
⊢ (⋂ i, t i).Nonempty
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case false
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (bif false then s else t)

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case true
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (bif true then s else t)

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
sd : s ⊆ t
ht : IsDiscrete t
tc : IsClosed[inst✝] t
⊢ IsClosed[inst✝] s

Tactic:
obtain ⟨_, rp, rt⟩ := isDiscrete_iff_forall_mem_exists_isClosed.mp ht s sd

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
sd : s ⊆ t
ht : IsDiscrete t
tc : IsClosed[inst✝] t
w✝ : Set X
rp : IsClosed[inst✝] w✝
rt : w✝ ∩ t = s
⊢ IsClosed[inst✝] s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s.Finite
⊢ IsClosed[inst✝¹] s

Tactic:
by
  rw [← biUnion_of_singleton s]
  exact hs.isClosed_biUnion fun i _ => isClosed_singleton

Goal state after:
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ T2Space X ↔ T0Space X

Tactic:
constructor <;> intro <;> infer_instance

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
⊢ s ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅

Tactic:
by
  simp only [mem_codiscreteWithin, disjoint_principal_right]
  refine ⟨fun h z hz ↦ ⟨(U \ s)ᶜ, h z hz, by simp⟩, fun h z hz ↦ ?_⟩
  rw [← exists_mem_subset_iff]
  obtain ⟨t, h₁t, h₂t⟩ := h z hz
  use t, h₁t, (disjoint_iff_inter_eq_empty.mpr h₂t).subset_compl_right

Goal state after:
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t

Tactic:
refine le_antisymm (nhdsSet_inter_le _ _) ?_

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ s ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : V ⊆ closure[inst✝] (V ∩ {x | IsPreirreducible (f ⁻¹' {x})})
U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
x : X
hxV : x ∈ f ⁻¹' V
hxU₁ : x ∈ U₁
y : X
hyV : y ∈ f ⁻¹' V
hyU₂ : y ∈ U₂
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty

Tactic:
obtain ⟨z, hzV, hz₁, hz₂⟩ :=
    hV _ _ (hf' _ hU₁) (hf' _ hU₂) ⟨f x, hxV, x, hxU₁, rfl⟩ ⟨f y, hyV, y, hyU₂, rfl⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : V ⊆ closure[inst✝] (V ∩ {x | IsPreirreducible (f ⁻¹' {x})})
U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
x : X
hxV : x ∈ f ⁻¹' V
hxU₁ : x ∈ U₁
y : X
hyV : y ∈ f ⁻¹' V
hyU₂ : y ∈ U₂
z : Y
hzV : z ∈ V
hz₁ : z ∈ f '' U₁
hz₂ : z ∈ f '' U₂
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ (∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 ∈ s ∪ {x} ↔ x_1 ∈ t ∪ {x}) ∧ (x ∈ s ∪ {x} ↔ x ∈ t ∪ {x})

Tactic:
union_singleton,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ (∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 ∈ insert x s ↔ x_1 ∈ insert x t) ∧ (x ∈ insert x s ↔ x ∈ insert x t)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ ∀ᶠ (x : X) in 𝓝[s] p, x ⤳ p

Tactic:
obtain ⟨t, h₁t, h₂t⟩ := disjoint_cofinite_right.mp hs
  set S := {y ∈ t ∩ s | ¬(y ⤳ p)}
  have hS_nhds (y) (hy : y ∈ S) : (closure ({y} : Set X))ᶜ ∈ 𝓝 p :=
    isClosed_closure.isOpen_compl.mem_nhds <| by
      simpa [specializes_iff_mem_closure] using hy.2
  filter_upwards [h₁t, nhdsWithin_le_nhds ((biInter_mem <| h₂t.subset (by grind)).mpr hS_nhds),
    self_mem_nhdsWithin] with x hxt hxS
  contrapose
  refine fun hxp hxf ↦ mem_iInter₂.mp hxS x ⟨⟨hxt, hxf⟩, hxp⟩ ?_
  grind [subset_closure]

Goal state after:
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
x y : X
h : ¬Inseparable x y
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝¹] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
← disjoint_nhds_nhds_iff_not_inseparable,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝¹] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
I : Finset ι
s : ι → Set X
hs : ∀ i ∈ I, DiscreteTopology ↑(s i)
hs' : ∀ i ∈ I, IsClosed[inst✝] (s i)
⊢ DiscreteTopology ↑(⋃ i ∈ I, s i)

Tactic:
simp only [← isDiscrete_iff_discreteTopology] at *
  exact .biUnion_finset hs hs'

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inl
α : Type u
inst✝ : TopologicalSpace α
x : α
t : Set α
H2 : x ∈ t
H4 : IsPreconnected t
r : Set α
H1 : x ∈ r
H3 : IsPreconnected r
⊢ x ∈ r

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inr
α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ x ∈ t

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inl
α : Type u
inst✝ : TopologicalSpace α
x : α
t : Set α
H2 : x ∈ t
H4 : IsPreconnected t
r : Set α
H1 : x ∈ r
H3 : IsPreconnected r
⊢ IsPreconnected r

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inr
α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ IsPreconnected t

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
⊢ T3Space X ↔ T0Space X

Tactic:
constructor <;> intro <;> infer_instance

Goal state after:
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case false
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (bif false then s else t)

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case true
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (bif true then s else t)

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected (connectedComponent x)

Tactic:
exact isPreconnected_connectedComponent

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected (connectedComponent (Classical.choice hα))

Tactic:
exact isPreconnected_connectedComponent

Goal state after:
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mp.a
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ IsPreconnected (connectedComponent x)

Tactic:
exact isPreconnected_connectedComponent

Goal state after:
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : ¬IsMeagre s
⊢ s.Nonempty

Tactic:
by
  contrapose! hs
  simpa [hs] using IsMeagre.empty

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous[inst✝³, inst✝²] ⇑f
⊢ Continuous[inst✝², inst✝³] ⇑f.symm

Tactic:
rw [continuous_iff_isClosed]
  intro C hC
  have hC' : IsClosed (f '' C) := (hC.isCompact.image hf).isClosed
  rwa [Equiv.image_eq_preimage_symm] at hC'

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

Goal state before:
pp: α : Type ua
u₁ u₂ : UniformSpace α
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
s✝ : Set (α × α)
⊢ s✝ ∈ 𝓤 α ↔ s✝ ∈ 𝓤 α

Tactic:
exact h _

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Tactic:
rw [cauchySeq_iff_tendsto] at hu

Goal state after:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : Tendsto (Prod.map u u) atTop (𝓤 α)
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
intro V mV

Goal state after:
case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
⊢ ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
F' : ι → α → β
hF : ∀ᶠ (x : ι) in p, ∀ (y : α), Inseparable (F x y) (F' x y)
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformly F' f p

Tactic:
← tendstoUniformlyOn_univ

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
F' : ι → α → β
hF : ∀ᶠ (x : ι) in p, ∀ (y : α), Inseparable (F x y) (F' x y)
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOn F' f p univ
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
b : Bool
x : ↑(S b)
hST : Disjoint (S b) (closure[inst✝¹.toTopologicalSpace] (S !b))
⊢ ∃ i, Disjoint (ball (↑x) ((B i).comp (B i).inv)) (S !b)

Tactic:
← disjoint_nhdsSet_principal,

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
b : Bool
x : ↑(S b)
hST : Disjoint (𝓝ˢ (S b)) (𝓟 (S !b))
⊢ ∃ i, Disjoint (ball (↑x) ((B i).comp (B i).inv)) (S !b)
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
b : Bool
x : ↑(S b)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x) U ⊆ (S !b)ᶜ
⊢ ∃ i, Disjoint (ball (↑x) ((B i).comp (B i).inv)) (S !b)

Tactic:
obtain ⟨(V : SetRel α α), hV, hVs, hVU⟩ := comp_symm_mem_uniformity_sets hUu

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
b : Bool
x : ↑(S b)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x) U ⊆ (S !b)ᶜ
V : SetRel α α
hV : V ∈ 𝓤 α
hVs : V.IsSymm
hVU : V.comp V ⊆ U
⊢ ∃ i, Disjoint (ball (↑x) ((B i).comp (B i).inv)) (S !b)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : α
⊢ 𝓝 s = comap (Prod.mk s) (𝓟 SetRel.id)

Tactic:
let _ : TopologicalSpace α := ⊥; have := discreteTopology_bot α
        simp [SetRel.id]

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

Goal state before:
pp: case left
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.fst f✝ (𝓝 x1)

Tactic:
assumption

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

Goal state before:
pp: case right
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.snd f✝ (𝓝 x2)

Tactic:
assumption

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), f x ≤ 𝓟 (U.preimage (t x))
⊢ ⨆ i, f i ≤ 𝓟 (⋃ i, U.preimage (t i))

Tactic:
← iSup_principal

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), f x ≤ 𝓟 (U.preimage (t x))
⊢ ⨆ i, f i ≤ ⨆ x, 𝓟 (U.preimage (t x))
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
⊢ map f = g

Tactic:
ext ⟨a⟩

Goal state after:
case mk
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
x✝ : SeparationQuotient α
a : α
⊢ map f (Quot.mk (⇑(inseparableSetoid α)) a) = g (Quot.mk (⇑(inseparableSetoid α)) a)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z | (f x, f z) ∈ t} ∩ {z | (g x, g z) ∈ t}
u_open : IsOpen[inst✝] u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, g x) ∈ t
I2 : (g x, g y) ∈ t
⊢ (f y, g y) ∈ r

Tactic:
exact htr (SetRel.prodMk_mem_comp I1 I2)

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
⊢ s m ∈ ⋃ y ∈ {k | k ≤ n}, {x | (x, s y) ∈ a}

Tactic:
mem_iUnion₂

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
⊢ ∃ i, ∃ (_ : i ∈ {k | k ≤ n}), s m ∈ {x | (x, s i) ∈ a}
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : β → α
hm : IsUniformInducing m
dense : DenseRange m
h : ∀ (f : Filter β), Cauchy f → ∃ x, map m f ≤ 𝓝 x
f : Filter α
hf : Cauchy f
p : Set (α × α) → Set α → Set α := fun s t ↦ {y | ∃ x ∈ t, (x, y) ∈ s}
g : Filter α := (𝓤 α).lift fun s ↦ f.lift' (p s)
mp₀ : Monotone p
mp₁ : ∀ {s : Set (α × α)}, Monotone (p s)
this✝⁵ : f ≤ g
this✝⁴ : g.NeBot
this✝³ : (comap m g).NeBot
this✝² : Cauchy g
this✝¹ : Cauchy (comap m g)
x : α
hx : map m (comap m g) ≤ 𝓝 x
this✝ : ClusterPt x (map m (comap m g))
this : ClusterPt x g
⊢ f ≤ g

Tactic:
assumption

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
l : Filter ι
inst✝ : l.IsCountablyGenerated
⊢ TendstoUniformly F f l ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformly (fun n ↦ F (u n)) f atTop

Tactic:
← tendstoUniformlyOn_univ

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
l : Filter ι
inst✝ : l.IsCountablyGenerated
⊢ TendstoUniformlyOn F f l univ ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n ↦ F (u n)) f atTop univ