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

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hf : ∀ (i : ι'), IsOpen[inst✝¹] (f i)
⊢ ∀ t ∈ range f, IsOpen[inst✝¹] t

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hf : ∀ (i : ι'), IsOpen[inst✝¹] (f i)
⊢ ⋂ i, f i = ⋂₀ range f

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
hT : ∀ t ∈ ∅, IsOpen[inst✝] t
T_count : ∅.Countable
⊢ ⋂₀ ∅ = ⋂ n, (fun _n ↦ univ) n

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen[inst✝] t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ∀ (n : ℕ), IsOpen[inst✝] (f n)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen[inst✝] t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ⋂₀ T = ⋂ n, f n

Tactic:
by

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

Goal state before:
pp: α : 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' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
⊢ f ⁻¹' T₂ = f ⁻¹' t ∩ v

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x}

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsGδ s ↔ ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ s = ⋂ n, f n

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X✝ : ι → Type u_2
inst✝⁴ : TopologicalSpace α
s t u v : Set α
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TotallyDisconnectedSpace Y
inst✝ : ConnectedSpace X
y : Y
⊢ Continuous[inst✝³, inst✝²] fun x ↦ y

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
s : ι' → Set X
hs : ∀ (i : ι'), IsGδ (s i)
⊢ IsGδ (⋂ i, s i)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
⊢ f '' (f ⁻¹' u ∩ s) = u

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ i, ⋂ (h : i ∈ s), t i h)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
h : ∀ s ∈ S, IsGδ s
hS : S.Countable
⊢ IsGδ (⋂₀ S)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∩ t)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
⊢ IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsEmbedding f
⊢ IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ TotallyDisconnectedSpace ↑s ↔ IsTotallyDisconnected s

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
h : ∀ s ∈ S, IsGδ s
⊢ IsGδ (⋃₀ S)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Finite
f : ι → Set X
h : ∀ i ∈ s, IsGδ (f i)
⊢ IsGδ (⋃ i ∈ s, f i)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : Continuous[inst✝¹, inst✝] f
hs : IsGδ s
⊢ IsGδ (f ⁻¹' s)

Tactic:
by

Goal state after:
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 (residual X)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
ho : IsGδ s
hd : Dense s
⊢ s ∈ residual X

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S ⊆ {t | IsOpen[inst✝] t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔
    ∃ S, (∀ t ∈ S, IsOpen[inst✝] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
⊢ IsTotallyDisconnected s

Tactic:
by

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

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

Tactic:
by

Goal state after:
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✝] t) ⊆ ∅

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed[inst✝] s
⊢ IsNowhereDense s ↔ interior s = ∅

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ∧ IsNowhereDense s ↔ IsOpen[inst✝] sᶜ ∧ Dense sᶜ

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsNowhereDense s ↔ ∀ x ∈ s, closure[inst✝] s ∉ 𝓝 x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : IsNowhereDense s
⊢ IsNowhereDense (f '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
⊢ TotallySeparatedSpace α ↔ Pairwise fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
h : Continuous[inst✝², inst✝¹] f
⊢ ∀ (a b : α), (connectedComponentSetoid α) a b → f a = f b

Tactic:
by

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

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

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
this : IsMeagre (⋃ i, f ↑i)
⊢ IsMeagre (⋃ i ∈ I, f i)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
⊢ TotallyDisconnectedSpace (ConnectedComponents α)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ IsCoinducing ⋯.connectedComponentsMap

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
⊢ IsMeagre (⋃ i ∈ I, f i)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
hf' : ∀ (y : β), IsConnected (f ⁻¹' {y})
⊢ Bijective ⋯.connectedComponentsMap

Tactic:
by

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

Goal state before:
pp: α : 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' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
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
⊢ t' ∈ T₁ ∪ T₂

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
this : F ⟨x, hx⟩ = F ⟨y, hy⟩
⊢ f x = f y

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
⊢ f x = f y

Tactic:
by

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

Goal state before:
pp: α : 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' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
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_decomp : t ⊆ T₁ ∪ T₂
⊢ Disjoint T₁ T₂

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
⊢ ∃ y ∈ T, EqOn f (const α y) S

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
h : IsDiscrete S
⊢ S.Subsingleton

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Finite X
f : ℕ → Set X
x✝¹ : ∀ (n : ℕ), IsOpen[inst✝¹] (f n)
x✝ : ∀ (n : ℕ), Dense (f n)
⊢ ∀ t ∈ range f, IsOpen[inst✝¹] t

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Finite X
f : ℕ → Set X
x✝¹ : ∀ (n : ℕ), IsOpen[inst✝¹] (f n)
x✝ : ∀ (n : ℕ), Dense (f n)
⊢ ∀ t ∈ range f, Dense t

Tactic:
by

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
n : ℕ
⊢ s ⊆ V n

Tactic:
by

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)
⊢ ⋂ n, g n ∩ V n = Subtype.val '' ⋂ n, f n

Tactic:
by

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
⊢ BaireSpace ↑s

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
by

Goal state after:
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:
by

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

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ ∀ t ∈ {s}, IsNowhereDense t

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ {s}.Countable

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ s ⊆ ⋃₀ {s}

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ IsMeagre s

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
A : ι → Set X
h : ¬IsMeagre (⋃ i ∈ I, A i)
⊢ ∃ i ∈ I, ¬IsMeagre (A i)

Tactic:
by

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

Goal state before:
pp: 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 := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ univ ⊆ interior (closure[inst✝²] s) ∪ (interior (closure[inst✝²] s))ᶜ

Tactic:
by

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

Goal state before:
pp: 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 := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ interior (closure[inst✝²] s) ∪ (interior (closure[inst✝²] s))ᶜ ⊆ closure[inst✝²] s ∪ (interior (closure[inst✝²] s))ᶜ

Tactic:
by

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

Goal state before:
pp: 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 := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ closure[inst✝²] (p '' f n) ⊆ closure[inst✝²] (p '' f n)

Tactic:
by

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

Goal state before:
pp: 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 := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ (interior (closure[inst✝²] s))ᶜ ⊆ closure[inst✝²] (closure[inst✝²] s)ᶜ

Tactic:
by

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

Goal state before:
pp: 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 := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ Dense (c n)

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ IsConnected (f ⁻¹' t)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : IsMeagre s
⊢ IsMeagre (f '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ IsConnected (f ⁻¹' connectedComponent t)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})
a : α
⊢ f '' connectedComponent a = connectedComponent (f a)

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α✝
s t u v : Set α✝
α : Type u_3
inst✝ : TopologicalSpace α
x : α
⊢ connectedComponent x = connectedComponent x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : Nonempty α
⊢ Nonempty (ConnectedComponents α)

Tactic:
by

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

Goal state before:
pp: 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 := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense (⋂ n, c n)
x : Y
h : ∀ (i : ℕ), x ∈ f i
i : ℕ
⊢ p x ∈ p '' f i ∨ p x ∉ closure[inst✝²] s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ IsEmpty (ConnectedComponents α) ↔ IsEmpty α

Tactic:
by

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

Goal state before:
pp: 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 := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense (⋂ n, c n)
⊢ ⋂ n, f n = p ⁻¹' ⋂ n, c n

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : PreconnectedSpace α
⊢ Subsingleton (ConnectedComponents α)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
⊢ BaireSpace Y

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
x : α
i : ι
hx : x ∈ U i
⊢ Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x

Tactic:
by

Goal state after: