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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : ∃ i, p i ∧ closure[inst✝¹] (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)

Tactic:
obtain ⟨i, hi, hi'⟩ := hT
    suffices closure (f '' s i) ∈ 𝓝 (f x) by filter_upwards [this] using hi'
    replace h := (h (s i)).mpr ⟨i, hi, Subset.rfl⟩
    exact hf.closure_image_mem_nhds h

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (C i)
t : Set ι
| (⋂ i ∈ t, C i)ᶜ = (⋂ i, C i)ᶜ

Tactic:
;

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (C i)
t : Set ι
| (⋂ i ∈ t, C i)ᶜ = (⋂ i, C i)ᶜ
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝²] (C i)
k : ℕ → ι
| (⋂ n, C (k n))ᶜ = (⋂ i, C i)ᶜ

Tactic:
;

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝²] (C i)
k : ℕ → ι
| (⋂ n, C (k n))ᶜ = (⋂ i, C i)ᶜ
Module: Mathlib.Topology.Connected.TotallyDisconnected

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

Tactic:
;

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
⊢ TotallyDisconnectedSpace α
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
ι' : Sort u_4
inst✝ : TopologicalSpace X
⊢ CountableInterFilter (countableGenerate {t | IsOpen[inst✝] t ∧ Dense t})

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
ι : Type u_3
ι' : Sort u_4
inst✝ : TopologicalSpace X
⊢ CountableInterFilter (countableGenerate {t | IsOpen[inst✝] t ∧ Dense t})
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
ht : t ⊆ s
hs : IsNowhereDense s
⊢ interior (closure[inst✝] s) ⊆ ∅

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
ht : t ⊆ s
hs : IsNowhereDense s
⊢ interior (closure[inst✝] s) ⊆ ∅
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inl
α : 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
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htu : f ⁻¹' {t'} ⊆ u
⊢ t' ∈ T₁

Tactic:
;

Goal state after:
case inl
α : 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
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htu : f ⁻¹' {t'} ⊆ u
⊢ t' ∈ T₁
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr
α : 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
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htv : f ⁻¹' {t'} ⊆ v
⊢ t' ∈ T₂

Tactic:
;

Goal state after:
case inr
α : 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
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htv : f ⁻¹' {t'} ⊆ v
⊢ t' ∈ T₂
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: case empty
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
ho : ∀ t ∈ ∅, IsOpen[inst✝] t
hd : ∀ t ∈ ∅, Dense t
⊢ Dense (⋂₀ ∅)

Tactic:
simp [sInter_empty]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set ↑s
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
g : ℕ → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst✝¹] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val ⁻¹' g n = f n
h_inter_dense : Dense (⋂ n, g n ∩ V n)
x✝ : X
⊢ x✝ ∈ ⋂ n, g n ∩ V n ↔ x✝ ∈ Subtype.val '' ⋂ n, f n

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set ↑s
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
g : ℕ → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst✝¹] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val ⁻¹' g n = f n
h_inter_dense : Dense (⋂ n, g n ∩ V n)
x✝ : X
⊢ x✝ ∈ ⋂ n, g n ∩ V n ↔ x✝ ∈ Subtype.val '' ⋂ n, f n
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
f : ℕ → Set ↑s
V : ℕ → Set X
hV✝ : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
g : ℕ → Set X
x✝ : X
hG : IsGδ (⋂ n, V n)
hd : Dense (⋂ n, V n)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
hV : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
hg1 : ∀ (n : ℕ), IsOpen[inst✝¹] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val ⁻¹' g n = f n
h_inter_dense : Dense (⋂ n, g n ∩ V n)
⊢ (∀ (i : ℕ), x✝ ∈ g i ∧ x✝ ∈ V i) ↔ ∃ (x : ∀ (i : ℕ), x✝ ∈ V i), ∀ (i : ℕ), ⟨x✝, ⋯⟩ ∈ f i

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
f : ℕ → Set ↑s
V : ℕ → Set X
hV✝ : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
g : ℕ → Set X
x✝ : X
hG : IsGδ (⋂ n, V n)
hd : Dense (⋂ n, V n)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
hV : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
hg1 : ∀ (n : ℕ), IsOpen[inst✝¹] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val ⁻¹' g n = f n
h_inter_dense : Dense (⋂ n, g n ∩ V n)
⊢ (∀ (i : ℕ), x✝ ∈ g i ∧ x✝ ∈ V i) ↔ ∃ (x : ∀ (i : ℕ), x✝ ∈ V i), ∀ (i : ℕ), ⟨x✝, ⋯⟩ ∈ f i
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst✝] x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ (compl '' compl '' S).Countable

Tactic:
;

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst✝] x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ (compl '' compl '' S).Countable
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: case h₁
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := ⋯
c : ℕ → Set X := ⋯
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ interior (closure[inst✝²] s) ⊆ closure[inst✝²] s

Tactic:
;

Goal state after:
case h₁
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := ⋯
c : ℕ → Set X := ⋯
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ interior (closure[inst✝²] s) ⊆ closure[inst✝²] s
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact (⇑h.symm '' s) ↔ IsCompact s

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact (⇑h.symm '' s) ↔ IsCompact s
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsSigmaCompact (⇑h.symm '' s) ↔ IsSigmaCompact s

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsSigmaCompact (⇑h.symm '' s) ↔ IsSigmaCompact s
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this : ⇑h.symm '' connectedComponentIn (⇑h '' s) (h x) ⊆ connectedComponentIn (⇑h.symm '' ⇑h '' s) (h.symm (h x))
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x

Tactic:
rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]
    at this

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
h : X ≃ₜ Y
⊢ LocallyCompactSpace X ↔ LocallyCompactSpace Y

Tactic:
by
  exact ⟨fun _ => h.symm.isOpenEmbedding.locallyCompactSpace,
    fun _ => h.isClosedEmbedding.locallyCompactSpace⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Constructions

Goal state before:
pp: M : Type u_1
inst✝¹ : TopologicalSpace M
inst✝ : Monoid M
⊢ TopologicalSpace.induced (Prod.fst ∘ ⇑(embedProduct M)) inst✝¹ ⊓
      TopologicalSpace.induced ((unop ∘ Prod.snd) ∘ ⇑(embedProduct M)) inst✝¹ =
    TopologicalSpace.induced val inst✝¹ ⊓ TopologicalSpace.induced (fun u ↦ ↑u⁻¹) inst✝¹

Tactic:
;

Goal state after:
M : Type u_1
inst✝¹ : TopologicalSpace M
inst✝ : Monoid M
⊢ TopologicalSpace.induced (Prod.fst ∘ ⇑(embedProduct M)) inst✝¹ ⊓
      TopologicalSpace.induced ((unop ∘ Prod.snd) ∘ ⇑(embedProduct M)) inst✝¹ =
    TopologicalSpace.induced val inst✝¹ ⊓ TopologicalSpace.induced (fun u ↦ ↑u⁻¹) inst✝¹
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y✝ : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y✝
inst✝⁵ : TopologicalSpace W
inst✝⁴ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : DecidablePred p
j : ι
⊢ Continuous[instTopologicalSpaceProd, inst✝¹ j] fun a ↦ if h : p j then a.1 ⟨j, h⟩ else a.2 ⟨j, h⟩

Tactic:
;

Goal state after:
X : Type u_1
Y✝ : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y✝
inst✝⁵ : TopologicalSpace W
inst✝⁴ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : DecidablePred p
j : ι
⊢ Continuous[instTopologicalSpaceProd, inst✝¹ j] fun a ↦ if h : p j then a.1 ⟨j, h⟩ else a.2 ⟨j, h⟩
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
x : X
⊢ ↑(hf.toHomeomorph (hf.toHomeomorph.symm ⟨f x, ⋯⟩)) = ↑(hf.toHomeomorph x)

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
x : X
⊢ ↑(hf.toHomeomorph (hf.toHomeomorph.symm ⟨f x, ⋯⟩)) = ↑(hf.toHomeomorph x)
Module: Mathlib.Topology.Algebra.Constructions

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
u : Mˣ
s : Set M
hs : s ∈ 𝓝 ((fun u ↦ ↑u⁻¹) u)
⊢ s ∈ Filter.map (fun u ↦ ↑u⁻¹) (𝓝 u)

Tactic:
simp only [← hf, nhds_induced, Filter.mem_map] at hs ⊢

Goal state after:
M : Type u_4
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
u : Mˣ
s : Set M
hs : s ∈ 𝓝 (f ↑u)
⊢ (fun u ↦ f ↑u) ⁻¹' s ∈ comap val (𝓝 ↑u)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst✝] u
v_op : IsOpen[inst✝] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' v)ᶜ

Tactic:
exact (v_op.preimage continuous_subtype_val).isClosed_compl

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

Goal state before:
pp: X : Type u_2
inst✝ : UniformSpace X
⊢ DiscreteUniformity X ↔ uniformity X = 𝓟 SetRel.id

Tactic:
discreteUniformity_iff_eq_bot,

Goal state after:
X : Type u_2
inst✝ : UniformSpace X
⊢ inst✝ = ⊥ ↔ uniformity X = 𝓟 SetRel.id
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case mk
α : Type ua
u₂ : UniformSpace α
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s ↦ s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this :
  { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }.toTopologicalSpace =
    u₂.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ } =
    u₂

Tactic:
;

Goal state after:
case mk
α : Type ua
u₂ : UniformSpace α
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s ↦ s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this :
  { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }.toTopologicalSpace =
    u₂.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ } =
    u₂
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case mk.mk
α : Type ua
toTopologicalSpace✝¹ : TopologicalSpace α
uniformity✝¹ : Filter (α × α)
symm✝¹ : Tendsto Prod.swap uniformity✝¹ uniformity✝¹
comp✝¹ : (uniformity✝¹.lift' fun s ↦ s ○ s) ≤ uniformity✝¹
nhds_eq_comap_uniformity✝¹ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝¹
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s ↦ s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this :
  { toTopologicalSpace := toTopologicalSpace✝¹, uniformity := uniformity✝¹, symm := symm✝¹, comp := comp✝¹,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, uniformity := uniformity✝¹, symm := symm✝¹, comp := comp✝¹,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type ua
toTopologicalSpace✝¹ : TopologicalSpace α
uniformity✝¹ : Filter (α × α)
symm✝¹ : Tendsto Prod.swap uniformity✝¹ uniformity✝¹
comp✝¹ : (uniformity✝¹.lift' fun s ↦ s ○ s) ≤ uniformity✝¹
nhds_eq_comap_uniformity✝¹ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝¹
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s ↦ s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this :
  { toTopologicalSpace := toTopologicalSpace✝¹, uniformity := uniformity✝¹, symm := symm✝¹, comp := comp✝¹,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, uniformity := uniformity✝¹, symm := symm✝¹, comp := comp✝¹,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }
Module: Mathlib.Topology.UniformSpace.Defs

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

Tactic:
;

Goal state after:
α : Type ua
u₁ u₂ : UniformSpace α
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
s✝ : Set (α × α)
⊢ s✝ ∈ 𝓤 α ↔ s✝ ∈ 𝓤 α
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)

Tactic:
;

Goal state after:
α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this : f.NeBot
⊢ Cauchy (f ×ˢ g)

Tactic:
;

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this : f.NeBot
⊢ Cauchy (f ×ˢ g)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f

Tactic:
;

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
| s ○ t

Tactic:
;

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
| s ○ t
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
fst✝ : α
snd✝ : γ
⊢ (fst✝, snd✝) ∈ s ○ t ↔ (fst✝, snd✝) ∈ ⋃ b, (fun p ↦ (p.1, b)) ⁻¹' s ∩ (fun p ↦ (b, p.2)) ⁻¹' t

Tactic:
;

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
fst✝ : α
snd✝ : γ
⊢ (fst✝, snd✝) ∈ s ○ t ↔ (fst✝, snd✝) ∈ ⋃ b, (fun p ↦ (p.1, b)) ⁻¹' s ∩ (fun p ↦ (b, p.2)) ⁻¹' t
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) atTop (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
;

Goal state after:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) atTop (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
⊢ ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

Tactic:
by
  rcases mem_atTop_sets.1 (hu (ball_mem_nhds a (symm_le_uniformity <| hV 0))) with ⟨n, hn⟩
  rcases (hu.comp (tendsto_add_atTop_nat n)).cauchySeq.subseq_mem fun n => hV (n + 1) with
    ⟨φ, φ_mono, hφV⟩
  exact ⟨fun k => φ k + n, φ_mono.add_const _, hn _ le_add_self, hφV⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ 𝓝 (a, b) = (𝓤 α).lift' fun s ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ s}

Tactic:
rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift']

Goal state after:
case hg₁
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ∀ (s : Set (α × α)), Monotone fun t ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ∀ (t : Set (α × α)), Monotone fun s ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
T : Set α
hx : x ∈ T
S : Set α
⊢ 𝓝[S] x = comap (Prod.mk x) (𝓤 α ⊓ 𝓟 (T ×ˢ S))

Tactic:
simp [nhdsWithin, nhds_eq_comap_uniformity, hx]

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

Goal state before:
pp: case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq fun n ↦ u (n + k)
⊢ CauchySeq u

Tactic:
rw [cauchySeq_iff] at h ⊢
    intro V mV
    obtain ⟨N, h⟩ := h V mV
    use N + k
    intro a ha b hb
    convert! h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb) <;> lia

Goal state after: