mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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

Goal state before:
pp: α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
⊢ DiscreteTopology α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
⊢ x ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ frontier {b | f b ≤ g b} ⊆ {b | f b = g b}

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ frontier {b | f b < g b} ⊆ {b | f b = g b}

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
⊢ s ⊆ v ∪ u

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
x✝ : x ∈ u ∪ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
cases hs xs with

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s : Set X
hs : IsCompact s
ι : Type u_3
t : Finset ι
U : ι → Set X
hU : ∀ i ∈ t, IsOpen[inst✝¹] (U i)
hsC : s ⊆ ⋃ i ∈ t, U i
⊢ ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected s

Tactic:
by

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

Goal state before:
pp: X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
⊢ R1Space X

Tactic:
by

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

Goal state before:
pp: X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ R1Space X

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderClosedTopology α
f g : β → α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst✝², inst✝⁵] f
hg : Continuous[inst✝², inst✝⁵] g
hf' : ContinuousOn f' {x | f x ≤ g x}
hg' : ContinuousOn g' {x | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
⊢ Continuous[inst✝², inst✝¹] fun x ↦ if f x ≤ g x then f' x else g' x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ Continuous[inst✝, inst✝³] fun b ↦ max (f b) (g b)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
⊢ IsPreconnected (⋃₀ c)

Tactic:
by

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✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ SeparatedNhds {f x} (f '' K \ interior s)

Tactic:
by

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:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ s_1 ∈ {s, t}, x ∈ s_1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ s_1 ∈ {s, t}, IsPreconnected s_1

Tactic:
by

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 (f i) a) l (𝓝 a)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
hs : IsPreconnected s
ht : IsPreconnected t
⊢ IsPreconnected (s ∪ t)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
Hs : IsConnected s
Ht : IsConnected t
⊢ IsConnected (s ∪ t)

Tactic:
by

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:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
⊢ IsPreconnected (⋃₀ S)

Tactic:
by

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✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ coclosedCompact X = cocompact X

Tactic:
by

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 (f i) a) l (𝓝[>] a)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∃ V, IsOpen[inst✝²] V ∧ K ⊆ V ∧ IsCompact (closure[inst✝²] V)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : WeaklyLocallyCompactSpace X
x : X
⊢ ∃ U, IsOpen[inst✝²] U ∧ x ∈ U ∧ IsCompact (closure[inst✝²] U)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x : α
⊢ Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), OrderClosedTopology (α i)
⊢ OrderClosedTopology ((i : ι) → α i)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
h : ReflTransGen R i j
⊢ ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
h : F ∈ 𝓝 x
⊢ connectedComponentIn F x ∈ 𝓝 x

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst✝¹] F
⊢ IsOpen[inst✝¹] (connectedComponentIn F x)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen[inst✝¹] (connectedComponent x)

Tactic:
by

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 : (i : ι) → i ∈ S → Set α
⊢ ⋂ i, ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
l : Filter α
inst✝¹ : CountableInterFilter l
inst✝ : Countable ι
p : α → ι → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i

Tactic:
by

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
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi

Tactic:
by

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:
by

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:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
⊢ IsPreconnected (⋃ n ∈ t, s n)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty) i j
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
⊢ ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ univ) i j

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty) i j
⊢ IsPreconnected (⋃ n, s n)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ LocallyConnectedSpace α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
x : α
⊢ ∀ (i : Set α), IsOpen[inst✝¹] i ∧ x ∈ i ∧ IsConnected i ↔ i ∈ {s | IsOpen[inst✝¹] s ∧ IsPreconnected s} ∧ x ∈ i

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : TopologicalSpace.IsTopologicalBasis {s | IsOpen[inst✝] s ∧ IsPreconnected s}
x✝ : α
⊢ ∀ (i : Set α), i ∈ {s | IsOpen[inst✝] s ∧ IsPreconnected s} ∧ x✝ ∈ i ↔ IsOpen[inst✝] i ∧ x✝ ∈ i ∧ IsConnected i

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
⊢ LocallyConnectedSpace β

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ LocallyConnectedSpace β

Tactic:
by

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

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

Tactic:
by

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

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✝¹ : LocallyConnectedSpace α
inst✝ : LocallyConnectedSpace β
⊢ LocallyConnectedSpace (α × β)

Tactic:
by

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

Goal state before:
pp: ι : 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
⊢ Filter α

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter ⊥

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter ⊤

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (comap f l)

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter α
inst✝ : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (map f l)

Tactic:
by

Goal state after:
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 : ι
hi : (s i).Nonempty
hj : (s j).Nonempty
⊢ TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
H : ∀ (n : β), IsPreconnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝¹ x✝ : β
⊢ ∀ i ∈ Ico x✝ x✝¹, (s (succ i) ∩ s i).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder β
inst✝² : SuccOrder β
inst✝¹ : IsSuccArchimedean β
inst✝ : Nonempty β
s : β → Set α
H : ∀ (n : β), IsConnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝¹ x✝ : β
⊢ ∀ i ∈ Ico x✝ x✝¹, (s (succ i) ∩ s i).Nonempty

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
⊢ CountableInterFilter (l₁ ⊓ l₂)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
⊢ LocallyConnectedSpace ((i : ι) → X i)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s t : Set α
hs : IsPreconnected s
ht : IsClopen t
hne : (s ∩ t).Nonempty
⊢ s ⊆ t ∪ tᶜ

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
⊢ CountableInterFilter (l₁ ⊔ l₂)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ IsConnected s ↔ ∃ i t, IsConnected t ∧ s = mk i '' t

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
x : (i : ι) → X i
this : ∀ (i : ι), Nonempty (X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ connectedComponent x
i : ι
hi : i ∈ {i | ¬PreconnectedSpace (X i)}
hiJ : i ∉ J
z : X i
x✝ : z ∈ univ
⊢ Function.eval i (Function.update x i z) = z

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = mk i '' t

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
⊢ ∀ (S : Set (Set (α × β))), S.Countable → (∀ s ∈ S, s ∈ l.curry m) → ⋂₀ S ∈ l.curry m

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
k : β
hk : k ∈ Ico j i
⊢ (s (succ k) ∩ s k).Nonempty

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ LocallyConnectedSpace ((i : ι) → X i) ↔
    IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
⊢ IsPreconnected (⋃ n ∈ t, s n)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
g : Set (Set α)
s✝ s : Set α
hs : s ∈ g
⊢ {s} ⊆ g ∧ {s}.Countable ∧ ⋂₀ {s} ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
g : Set (Set α)
s : Set α
⊢ ∅ ⊆ g ∧ ∅.Countable ∧ ⋂₀ ∅ ⊆ univ

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ IsConnected s ↔ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t

Tactic:
by

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

Goal state before:
pp: α : 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, ⋃ (H : s ∈ S), T s H ⊆ g

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : f '' s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ IsPreconnected s ↔ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t

Tactic:
by

Goal state after: