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

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
set f : (Σ I : Finset ι, ∀ i : I, t i) → ∀ i, X i := fun ⟨I, g⟩ i ↦
      if hi : i ∈ I then g ⟨i, hi⟩ else (default : ∀ i, X i) i
    refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
    rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩
    have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦
      (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩
    choose y hyt hyu using this
    lift y to ∀ i : I, t i using hyt
    refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩
    simp only [f, dif_pos hi]
    exact hyu ⟨i, _⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
⊢ SecondCountableTopology α

Tactic:
rcases @SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
⊢ SecondCountableTopology α
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ (⋃ u ∈ s', f u).Countable

Tactic:
apply s'_count.biUnion

Goal state after:
case refine_1
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ∀ a ∈ s', (f a).Countable
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: 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
⊢ (f ⁻¹' ⋃ n, L n) ∩ s = f ⁻¹' f '' s ∩ s

Tactic:
by rw [hcov]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
inst✝¹ : SigmaCompactSpace X
inst✝ : SigmaCompactSpace Y
⊢ ⋃ n, (fun n ↦ compactCovering X n ×ˢ compactCovering Y n) n = univ

Tactic:
by
      simp only [iUnion_prod_of_monotone (compactCovering_subset X) (compactCovering_subset Y),
        iUnion_compactCovering, univ_prod_univ]

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
⊢ univ.Countable

Tactic:
have := fun n => hf.finite_nonempty_inter_compact (isCompact_compactCovering X n)
  refine (countable_iUnion fun n => (this n).countable).mono fun i _ => ?_
  rcases hne i with ⟨x, hx⟩
  rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering X) x with ⟨n, hn⟩
  exact mem_iUnion.2 ⟨n, x, hx, hn⟩

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

Goal state before:
pp: case refine_1
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Monotone fun f ↦ ∃ x ∈ s, ClusterPt x f

Tactic:
rintro f g hle ⟨x, hxs, hxf⟩
    exact ⟨x, hxs, hxf.mono hle⟩

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
s : Set (Set X)
hsc : ∀ t ∈ s, IsClosed[inst✝¹] t
hs : ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
⊢ (⋂₀ s).Nonempty

Tactic:
simpa using isCompact_univ.nonempty_inter_sInter hsc (by simpa using hs)

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
inst✝ : IndiscreteTopology X
u v : Set X
⊢ u = ∅ ∨ u = univ → v = ∅ ∨ v = univ → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty

Tactic:
rintro ⟨h | h⟩

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
inst✝ : IndiscreteTopology X
v : Set X
⊢ v = ∅ ∨ v = univ → ∅.Nonempty → v.Nonempty → (∅ ∩ v).Nonempty

case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
inst✝ : IndiscreteTopology X
u v : Set X
h✝ : u = univ
⊢ v = ∅ ∨ v = univ → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
⊢ (S ∩ b).Nonempty → (S ∩ (a ∩ b)).Nonempty

Tactic:
bS

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
⊢ (S ∩ (a ∩ b)).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ Z ⊆ closure[inst✝] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ

Tactic:
rw [← Set.inter_eq_right.mpr h]
    apply subset_closure_inter_of_isPreirreducible_of_isOpen hZ.1.2
    · rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]
      exact hX.sdiff.isClosed_biUnion fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1
    · rw [Set.inter_compl_nonempty_iff]
      exact mt (mem_of_subset_sUnion_irreducibleComponents Z hZ _ hX.sdiff Set.sdiff_subset)
        (Set.notMem_sdiff_of_mem (Set.mem_singleton Z))

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

Goal state before:
pp: case inl
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
ι : Type u_4
X : ι → Type u_3
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (a : ι), T2Space (X a)
i : ι
x y : X i
ne : x ≠ y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ ⟨i, x⟩ ∈ u ∧ ⟨i, y⟩ ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_isOpenEmbedding .sigmaMk ne

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
s : Set X
x✝ : IsClosed[inst✝²] s
h2s : s.Nonempty
⊢ IsClosed[inst✝¹] (const X y '' s)

Tactic:
const,

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
s : Set X
x✝ : IsClosed[inst✝²] s
h2s : s.Nonempty
⊢ IsClosed[inst✝¹] ((fun a ↦ y) '' s)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∈ U \ s
⊢ (insert z t ∩ (U \ s)).Finite

pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∉ U \ s
⊢ (insert z t ∩ (U \ s)).Finite

Tactic:
· rw [inter_comm, inter_insert_of_mem hz, inter_comm, h₂t]
      simp

Goal state after:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∉ U \ s
⊢ (insert z t ∩ (U \ s)).Finite
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) → ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite

Tactic:
intro h z h₁z
    obtain ⟨t, h₁t, h₂t⟩ := h z h₁z
    use insert z t, insert_mem_nhds_iff.mpr h₁t
    by_cases hz : z ∈ U \ s
    · rw [inter_comm, inter_insert_of_mem hz, inter_comm, h₂t]
      simp
    · rw [inter_comm, inter_insert_of_notMem hz, inter_comm, h₂t]
      simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a

Tactic:
by
  rw [← nhdsWithin_union, Iio_union_Ici, nhdsWithin_univ]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ S ∈ codiscrete X ↔ IsOpen[inst✝] S ∧ IsDiscrete Sᶜ

Tactic:
rw [mem_codiscrete, ← isClosed_compl_iff, isClosed_and_discrete_iff]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
⊢ closure[inst✝¹] K ⊆ U

Tactic:
by
  rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]
  exact fun x hx y hxy ↦ (hxy.mem_open_iff hU).1 (hKU hx)

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

Goal state before:
pp: α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
⊢ a ∉ range f

Tactic:
rw [mem_range]

Goal state after:
α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
⊢ ¬∃ y, f y = a
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
a b : α
⊢ Ioo a b ⊆ closure[inst✝²] (interior (Ioo a b))

Tactic:
simp only [interior_Ioo, subset_closure]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun i ↦ max a (f i)) l (𝓝 a)

Tactic:
simpa only [sup_idem] using (tendsto_const_nhds (x := a)).max h

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

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ i, ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h

Tactic:
simp only [biUnion_eq_iUnion]

Goal state after:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x✝ : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hU : ∀ (u v : Set α), u ∈ ∅ → v ∈ ∅ → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ ∅, IsOpen[inst✝] u
hsU : s ⊆ ⋃₀ ↑∅
⊢ s ⊆ ∅

Tactic:
by simpa using hsU

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

Goal state before:
pp: case neg
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst✝] u
h'u : (s ∩ u).Nonempty
h : closure[inst✝] u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
⊢ x ∈ u ∪ (closure[inst✝] u)ᶜ

Tactic:
· right
      intro h'x
      exact xu (h (mem_inter h'x hx))

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
⊢ (𝓝ˢ K).lift' closure[inst✝¹] = 𝓝ˢ K

Tactic:
refine le_antisymm (fun U hU ↦ ?_) (le_lift'_closure _)
  rcases hK.exists_isOpen_closure_subset hU with ⟨V, hVo, hKV, hVU⟩
  exact mem_of_superset (mem_lift' <| hVo.mem_nhdsSet.2 hKV) hVU

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a))
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)

Tactic:
rw [← di.nhds_eq_comap] at lim2

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ 𝓝 a
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsLindelof s ↔ IsLindelof univ

Tactic:
by
  rw [Subtype.isLindelof_iff, image_univ, Subtype.range_coe]

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

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (closure[inst✝²] (SeparationQuotient.mk ⁻¹' s)) (SeparationQuotient.mk ⁻¹' t)

Tactic:
← preimage_mk_closure

Goal state after:
case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (SeparationQuotient.mk ⁻¹' closure s) (SeparationQuotient.mk ⁻¹' t)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (SeparationQuotient.mk ⁻¹' s) (closure[inst✝²] (SeparationQuotient.mk ⁻¹' t))

Tactic:
← preimage_mk_closure

Goal state after:
case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (SeparationQuotient.mk ⁻¹' s) (SeparationQuotient.mk ⁻¹' closure t)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, ↑i) → ∃ x_1, ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, ↑i).Nonempty
si : Finset { s // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, ↑i).Nonempty
⊢ ⋂ U ∈ si, ↑U ⊆ u ∪ v

Tactic:
rwa [← disjoint_compl_left_iff_subset, disjoint_iff_inter_eq_empty,
        ← not_nonempty_iff_eq_empty]

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 : α → β
p : Filter ι
p' : Filter α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', Inseparable (F n.1 n.2) (F' n.1 n.2)
⊢ TendstoUniformlyOnFilter F' f p p'

Tactic:
rw [tendstoUniformlyOnFilter_iff_tendsto, uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
F' : ι → α → β
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ p', (f x.2, F x.1 x.2) ∈ id i
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', Inseparable (F n.1 n.2) (F' n.1 n.2)
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ p', (f x.2, F' x.1 x.2) ∈ id i
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
⊢ (𝓤 α).HasBasis (fun V ↦ V ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] V ∧ V.IsSymm) id

Tactic:
by
  simp only [← and_assoc]
  refine uniformity_hasBasis_open.restrict fun s hs => ⟨SetRel.symmetrize s, ?_⟩
  exact
    ⟨⟨symmetrize_mem_uniformity hs.1, IsOpen.inter hs.2 (hs.2.preimage continuous_swap)⟩,
      inferInstance, SetRel.symmetrize_subset_self⟩

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

Goal state before:
pp: α : Type ua
s : Set (UniformSpace α)
⊢ (sInf s).toTopologicalSpace = ⨅ i ∈ s, i.toTopologicalSpace

Tactic:
by
  rw [sInf_eq_iInf]
  simp only [← toTopologicalSpace_iInf]

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
this : x = y
⊢ x ∈ s

Tactic:
by rwa [this]

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 : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))

Tactic:
rw [eventually_prod_iff]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∃ pa,
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : α) in p', pb y) ∧
          ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → Tendsto (fun n ↦ F n (x, y).2) p (𝓝 (f (x, y).2))
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

Tactic:
rw [Filter.eventually_swap_iff]

Goal state after:
case inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
⊢ ⊥.TotallyBounded

Tactic:
← principal_empty,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
⊢ (𝓟 ∅).TotallyBounded
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology α
⊢ u = ⊤

Tactic:
refine UniformSpace.ext ?_

Goal state after:
α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology α
⊢ 𝓤 α = 𝓤 α
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ map ((fun x ↦ (g x.1, g x.2)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ ↔
    map (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ

Tactic:
comp_def,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ map (fun x ↦ (g (f x.1, f x.2).1, g (f x.1, f x.2).2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ ↔
    map (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × γ) in (p ×ˢ p) ×ˢ comap g p', ((fun n ↦ F n ∘ g) m.1.1 m.2, (fun n ↦ F n ∘ g) m.1.2 m.2) ∈ u

Tactic:
rw [eventually_prod_iff]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∃ pa,
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : γ) in comap g p', pb y) ∧
          ∀ {x : ι × ι},
            pa x → ∀ {y : γ}, pb y → ((fun n ↦ F n ∘ g) (x, y).1.1 (x, y).2, (fun n ↦ F n ∘ g) (x, y).1.2 (x, y).2) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ (∀ x ∈ Iic (𝓟 s), Cauchy x → ∃ x_1 ∈ s, map m x ≤ 𝓝 (m x_1)) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x

Tactic:
map_le_iff_le_comap,

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ (∀ x ∈ Iic (𝓟 s), Cauchy x → ∃ x_1 ∈ s, x ≤ comap m (𝓝 (m x_1))) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
⊢ u = u'

Tactic:
refine UniformSpace.ext ?_

Goal state after:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
⊢ 𝓤 γ = 𝓤 γ