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

Goal state before:
pp: case mpr.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ⋃ n, (fun n ↦ f ⁻¹' L n ∩ s) n = s

Tactic:
· calc ⋃ n, f ⁻¹' L n ∩ s
        _ = f ⁻¹' (⋃ n, L n) ∩ s := by rw [preimage_iUnion, iUnion_inter]
        _ = f ⁻¹' (f '' s) ∩ s := by rw [hcov]
        _ = s := inter_eq_right.mpr (subset_preimage_image _ _)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s

Tactic:
let ⟨t, ht⟩ := hs.elim_nhds_subcover_nhdsSet' (fun x _ => U x) hU

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset ↑s
ht : ⋃ x ∈ t, U ↑x ∈ 𝓝ˢ s
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
x✝ : Filter X
hf : x✝.NeBot
hfa : x✝ ≤ 𝓟 {x}
⊢ 𝓟 {x} ≤ 𝓝 x

Tactic:
by simpa only [principal_singleton] using pure_le_nhds x

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ BddBelow ↑(upperClosure s) ↔ BddBelow s

Tactic:
simp_rw [BddBelow, lowerBounds_upperClosure]

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∉ t
b : α
hb : b ∈ t
hab : a ≤ b
⊢ False

Tactic:
exact hat <| hst _ ha _ hb hab

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Type v
inst✝ : CompactSpace X
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝¹] (t i)
hst : ∀ (s : Finset ι), (⋂ i ∈ s, t i).Nonempty
⊢ ∀ (u : Finset ι), (univ ∩ ⋂ i ∈ u, t i).Nonempty

Tactic:
simpa using hst

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (f '' univ)

Tactic:
image_univ

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (range f)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case h.refine_3.htd
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
U : Set X
hU : U ∈ c
U' : Set X
hU' : U' ∈ c
V : Set X
hVc : V ∈ c
hVU : U ⊆ V
hVU' : U' ⊆ V
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ (↑i)ᶜ) ⟨U, hU⟩) ((fun i ↦ (↑i)ᶜ) z) ∧
      (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ (↑i)ᶜ) ⟨U', hU'⟩) ((fun i ↦ (↑i)ᶜ) z)

Tactic:
exact ⟨⟨V, hVc⟩, Set.compl_subset_compl.mpr hVU, Set.compl_subset_compl.mpr hVU'⟩

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

Goal state before:
pp: case mk.mk
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
i✝ : T2Quotient X
x : X
j✝ : T2Quotient X
y : X
h : ¬mk x = mk y
s : Setoid X
hs : T2Space (Quotient s)
hsxy : ⟦x⟧ ≠ ⟦y⟧
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Quot.mk (⇑(t2Setoid X)) x ∈ u ∧ Quot.mk (⇑(t2Setoid X)) y ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_continuous (continuous_map_sInf (by exact hs)) hsxy

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen[inst✝¹] o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ o \ {y} ∩ s ⊆ t

Tactic:
exact (inter_subset_inter sdiff_subset Subset.rfl).trans host

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
x y : X
xspecy : x ⤳ y
⊢ y ⤳ x

pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Std.Symm Specializes → ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y

Tactic:
· rw [← IsInducing.specializes_iff isInducing_mk, h xspecy] at *

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Std.Symm Specializes → ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
⊢ codiscrete X ≤ cofinite

Tactic:
intro s

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
⊢ s ∈ cofinite → s ∈ codiscrete X
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
⊢ cofinite ⊓ 𝓟 K ≤ codiscreteWithin K

Tactic:
intro s

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
s : Set X
⊢ s ∈ codiscreteWithin K → s ∈ cofinite ⊓ 𝓟 K
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s | sᶜ ∈ l}
⊢ ∀ s ∈ compl '' S, s ∈ l

Tactic:
intro s

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s | sᶜ ∈ l}
s : Set α
⊢ s ∈ compl '' S → s ∈ l
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
hs : IsPreconnected (⋃ n, s n)
hs' : ∀ (i : ι), IsOpen[inst✝] (s i)
i j : ι
hij : ¬TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j
S : Set ι := {k | TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i k}
U : Set α := ⋃ k ∈ S, s k
V : Set α := ⋃ k ∈ Sᶜ, s k
hsplit : ⋃ n, s n = U ∪ V
a : α
ha : a ∈ s i
b : α
hb : b ∈ s j
hi_S : i ∈ S := TransGen.single (Exists.intro a ⟨ha, ha⟩)
hUne : ((⋃ n, s n) ∩ U).Nonempty
hVne : ((⋃ n, s n) ∩ V).Nonempty
x : α
k : ι
hk : k ∈ S
hxk : x ∈ s k
l : ι
hl : l ∉ S
hxl : x ∈ s l
⊢ False

Tactic:
exact hl (hk.tail ⟨x, hxk, hxl⟩)

Goal state after:
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mp.sInter
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : S.Countable
a✝ : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∀ t' ∈ S, ⋂₀ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ t'

Tactic:
intro s

Goal state after:
case mp.sInter
α : Type u_2
g : Set (Set α)
s✝ : Set α
S : Set (Set α)
Sct : S.Countable
a✝ : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
s : Set α
⊢ s ∈ S → ⋂₀ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ s
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mpr
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : S.Countable
hS : ⋂₀ S ⊆ s
⊢ ∀ s ∈ S, s ∈ countableGenerate g

Tactic:
intro s

Goal state after:
case mpr
α : Type u_2
g : Set (Set α)
s✝ : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : S.Countable
hS : ⋂₀ S ⊆ s✝
s : Set α
⊢ s ∈ S → s ∈ countableGenerate g
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
⊢ f ≤ countableGenerate g

Tactic:
intro s

Goal state after:
case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
⊢ s ∈ countableGenerate g → s ∈ f
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsu with ⟨x, hxs, hxu⟩

Goal state after:
case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
x : α
hxs : x ∈ s
hxu : x ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsu with ⟨x, hxs, hxu⟩

Goal state after:
case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
x : α
hxs : x ∈ s
hxu : x ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
x✝¹ : Filter X
hf : x✝¹.NeBot
x✝ : CountableInterFilter x✝¹
hfa : x✝¹ ≤ 𝓟 {x}
⊢ 𝓟 {x} ≤ 𝓝 x

Tactic:
by simpa only [principal_singleton] using pure_le_nhds x

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyNormalSpace X
s t : Set X
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
hd : Disjoint s t
⊢ Disjoint s (closure[inst✝¹] t)

Tactic:
ht.closure_eq

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyNormalSpace X
s t : Set X
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
hd : Disjoint s t
⊢ Disjoint s t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case a.left
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := ⋯
T₂ : Set β := ⋯
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
a : α
hat : a ∈ f ⁻¹' t
hau : a ∈ u
⊢ f a ∈ t

pp: case a.right
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := ⋯
T₂ : Set β := ⋯
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
a : α
hat : a ∈ f ⁻¹' t
hau : a ∈ u
⊢ f ⁻¹' {f a} ⊆ u

Tactic:
· exact mem_preimage.1 hat

Goal state after:
case a.right
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := ⋯
T₂ : Set β := ⋯
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
a : α
hat : a ∈ f ⁻¹' t
hau : a ∈ u
⊢ f ⁻¹' {f a} ⊆ u
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof (f '' univ)

Tactic:
image_univ

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof (range f)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case inl
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝²] (U i)
htc : ∅.Countable
htu : ⋃ i ∈ ∅, U i = ⋃ i, U i
⊢ ∃ k, ⋃ n, U (k n) = ⋃ i, U i

Tactic:
mem_empty_iff_false,

Goal state after:
case inl
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝²] (U i)
htc : ∅.Countable
htu : ⋃ i, ⋃ (_ : False), U i = ⋃ i, U i
⊢ ∃ k, ⋃ n, U (k n) = ⋃ i, U i
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case a.left
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := ⋯
T₂ : Set β := ⋯
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
⊢ f a ∈ t

pp: case a.right
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := ⋯
T₂ : Set β := ⋯
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
⊢ f ⁻¹' {f a} ⊆ v

Tactic:
· exact mem_preimage.1 hat

Goal state after:
case a.right
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := ⋯
T₂ : Set β := ⋯
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
⊢ f ⁻¹' {f a} ⊆ v
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
⊢ IsTotallyDisconnected univ

Tactic:
intro s

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
⊢ s ⊆ univ → IsPreconnected s → s.Subsingleton
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsMeagre ∅

Tactic:
IsMeagre,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∅ᶜ ∈ residual X
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsMeagre s
ht : IsMeagre t
⊢ IsMeagre (s ∪ t)

Tactic:
IsMeagre,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsMeagre s
ht : IsMeagre t
⊢ (s ∪ t)ᶜ ∈ residual X
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hs : ∀ (i : ι'), IsMeagre (f i)
⊢ IsMeagre (⋃ i, f i)

Tactic:
IsMeagre,

Goal state after:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hs : ∀ (i : ι'), IsMeagre (f i)
⊢ (⋃ i, f i)ᶜ ∈ residual X
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsMeagre s ↔ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
IsMeagre,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ residual X ↔ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ s, ↑s = ∅
V : Set (ConnectedComponents X)
hU : IsClopen V
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v

Tactic:
refine ⟨Vᶜ, V, hU.compl.isOpen, hU.isOpen, ?_, hb mem_connectedComponent, disjoint_compl_left⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ s, ↑s = ∅
V : Set (ConnectedComponents X)
hU : IsClopen V
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
⊢ mk a ∈ Vᶜ
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr.succ
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
hn : 0 < n + 1
⊢ ∃ U,
    (∀ (i : Fin (n + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
clear hn

Goal state after:
case inr.succ
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
⊢ ∃ U,
    (∀ (i : Fin (n + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ
Module: Mathlib.Topology.UniformSpace.DiscreteUniformity

Goal state before:
pp: X : Type u_2
inst✝ : UniformSpace X
⊢ (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ uniformity X) ↔ ∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ 𝓟 SetRel.id

Tactic:
bot_uniformity

Goal state after:
X : Type u_2
inst✝ : UniformSpace X
⊢ (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ 𝓟 SetRel.id) ↔ ∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ 𝓟 SetRel.id
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
⊢ l.NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun p ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)

Tactic:
prod_map_map_eq,

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
⊢ l.NeBot ∧ map (fun p ↦ (f p.1, f p.2)) (l ×ˢ l) ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun p ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
⊢ f ≤ 𝓝 x

Tactic:
intro s

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
⊢ s ∈ 𝓝 x → s ∈ f
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ⊆ s

Tactic:
obtain ⟨w, w_in, w_sub⟩ : ∃ w ∈ 𝓤 α, w ○ w ⊆ s := comp_mem_uniformity_sets hs
  use SetRel.symmetrize w, symmetrize_mem_uniformity w_in, inferInstance
  have : SetRel.symmetrize w ⊆ w := SetRel.symmetrize_subset_self
  calc SetRel.symmetrize w ○ SetRel.symmetrize w
    _ ⊆ w ○ w := by gcongr
    _ ⊆ s := w_sub

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun p ↦ (u p.1, u p.2)) (atTop ×ˢ atTop) (𝓤 α) ↔ Tendsto (Prod.map u u) atTop (𝓤 α)

Tactic:
by simp only [prod_atTop_atTop_eq, Prod.map_def]

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

Goal state before:
pp: case succ
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : SetRel α α}, s ∈ 𝓤 α → ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝ + 1] t ⊆ s

Tactic:
refine (ihn htU).mono fun U hU => ?_

Goal state after:
case succ
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : SetRel α α}, s ∈ 𝓤 α → ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun x ↦ U ○ x)^[n✝] U ⊆ t
⊢ U ⊆ s ∧ (fun x ↦ U ○ x)^[n✝ + 1] U ⊆ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
⊢ Tendsto (Prod.map f f) atTop (𝓤 α)

Tactic:
intro s

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
⊢ s ∈ 𝓤 α → s ∈ map (Prod.map f f) atTop
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
S : Set α
hS : S ∈ f
T : Set α
hT : T ∈ f
H : S ×ˢ T ⊆ SetRel.id
⊢ ∃ x, f = pure x

Tactic:
obtain ⟨x, rfl, _, _, _⟩ := SetRel.exists_eq_singleton_of_prod_subset_id
    (f_ne_bot.nonempty_of_mem hS) (f_ne_bot.nonempty_of_mem hT) H

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
x : α
hS hT : {x} ∈ f
H : {x} ×ˢ {x} ⊆ SetRel.id
⊢ ∃ x, f = pure x
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f

Tactic:
rcases comp_symm_of_uniformity hU with ⟨r, hr, rs, rU⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
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 : ι), U.preimage (t x) ∈ f x
⊢ ∃ t, t.Finite ∧ U.preimage t ∈ ⨆ i, f i

Tactic:
refine ⟨⋃ i, t i, finite_iUnion htf, ?_⟩

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 : ι), U.preimage (t x) ∈ f x
⊢ U.preimage (⋃ i, t i) ∈ ⨆ i, f i
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ IsComplete univ ↔ IsComplete (range f)

Tactic:
← isComplete_image_iff hf,

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ IsComplete (f '' univ) ↔ IsComplete (range f)