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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
F : Set β
hF : IsOpen[inst✝] F
y : β
x✝ : y ∈ F
⊢ IsOpen[inst✝²] (⋃ x ∈ f ⁻¹' connectedComponentIn F y, connectedComponentIn (f ⁻¹' F) x)

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
F : Set β
hF : IsOpen[inst✝] F
y : β
x✝ : y ∈ F
⊢ IsOpen[inst✝²] (⋃ x ∈ f ⁻¹' connectedComponentIn F y, connectedComponentIn (f ⁻¹' F) x)
Module: Mathlib.Order.Filter.CountableInter

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

Tactic:
]

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s | sᶜ ∈ l}
s : Set α
hs : ∃ x ∈ S, xᶜ = s
⊢ s ∈ l
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 β
⊢ ∀ (x : α × β), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
]

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : LocallyConnectedSpace α
inst✝ : LocallyConnectedSpace β
⊢ ∀ (x : α × β), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
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 β
x : α
y : β
U : Set (α × β)
hU : U ∈ 𝓝 (x, y)
u : Set α
hu : u ∈ 𝓝 x
v : Set β
hv : v ∈ 𝓝 y
huv : u ×ˢ v ⊆ U
⊢ ∃ V ∈ 𝓝 (x, y), IsPreconnected V ∧ V ⊆ U

Tactic:
exact ⟨connectedComponentIn u x ×ˢ connectedComponentIn v y,
    prod_mem_nhds (connectedComponentIn_mem_nhds hu) (connectedComponentIn_mem_nhds hv),
    isPreconnected_connectedComponentIn.prod isPreconnected_connectedComponentIn,
    (prod_mono (connectedComponentIn_subset _ _) (connectedComponentIn_subset _ _)).trans huv⟩

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
x : (i : ι) → X i
U : Set ((i : ι) → X i)
hU : ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ I.pi t ⊆ U
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
hU : ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ I.pi t ⊆ U
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Module: Mathlib.Order.Filter.CountableInter

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

Tactic:
]

Goal state after:
case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ tᶜ ∈ l
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
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
⊢ IsPreconnected (univ.pi (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) fun x ↦ univ))

Tactic:
]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
⊢ IsPreconnected (univ.pi (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) fun x ↦ univ))
Module: Mathlib.Order.Filter.CountableInter

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

Tactic:
]

Goal state after:
case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : tᶜ ⊆ sᶜ
⊢ tᶜ ∈ l
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:
]

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter (𝓟 ∅)
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter (𝓟 univ)

Tactic:
]

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter (𝓟 univ)
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case pos
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
hi : i ∈ K
⊢ IsPreconnected (connectedComponentIn (t i) (x i))

Tactic:
]

Goal state after:
case pos
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
hi : i ∈ K
⊢ IsPreconnected (connectedComponentIn (t i) (x i))
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case neg
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
hi : i ∉ K
⊢ IsPreconnected univ

Tactic:
]

Goal state after:
case neg
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
hi : i ∉ K
⊢ IsPreconnected univ
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₂
S : Set (Set α)
hSc : S.Countable
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ i, ⋂ (h : i ∈ S), s i h ∈ l₁
ht : ⋂ i, ⋂ (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ (⋂ i, ⋂ (h : i ∈ S), s i h) ∩ ⋂ i, ⋂ (h : i ∈ S), t i h ⊆ s i hi ∩ t i hi

Tactic:
]

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ i, ⋂ (h : i ∈ S), s i h ∈ l₁
ht : ⋂ i, ⋂ (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ (⋂ i, ⋂ (h : i ∈ S), s i h) ∩ ⋂ i, ⋂ (h : i ∈ S), t i h ⊆ s i hi ∩ t i hi
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
⊢ ⋂₀ S ∈ l₁

Tactic:
refine (countable_sInter_mem hSc).2 fun s hs => ?_

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₁
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
⊢ ⋂₀ S ∈ l₂

Tactic:
refine (countable_sInter_mem hSc).2 fun s hs => ?_

Goal state after:
case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₂
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 k ∩ s (succ k)).Nonempty

Tactic:
]

Goal state after:
α : 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 k ∩ s (succ k)).Nonempty
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case refine_1.inr
ι : 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)
hVn : ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ I.pi t ⊆ connectedComponent x
⊢ {i | ¬PreconnectedSpace (X i)}.Finite

Tactic:
]

Goal state after:
case refine_1.inr
ι : 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)
hVn : ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ I.pi t ⊆ connectedComponent x
⊢ {i | ¬PreconnectedSpace (X i)}.Finite
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case refine_1.inr
ι : 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
j : ι
hj : j ∈ J
⊢ x j ∈ t j

Tactic:
]

Goal state after:
case refine_1.inr
ι : 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
j : ι
hj : j ∈ J
⊢ x j ∈ t j
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 : s ⊆ f ⁻¹' u ∪ f ⁻¹' 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:
]

Goal state after:
α : 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 : s ⊆ f ⁻¹' u ∪ f ⁻¹' 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'
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
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
huv : s ⊆ (u' ∪ v') ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
]

Goal state after:
α : 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
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
huv : s ⊆ (u' ∪ v') ∩ s
⊢ s ⊆ u' ∪ v'
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst✝², instTopologicalSpaceSigma] f
i : ι
hi : range f ⊆ range (Sigma.mk i)
⊢ ∃ i g, Continuous[inst✝², inst✝ i] g ∧ f = Sigma.mk i ∘ g

Tactic:
rcases range_subset_range_iff_exists_comp.1 hi with ⟨g, rfl⟩

Goal state after:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
g : α → X i
hf : Continuous[inst✝², instTopologicalSpaceSigma] (Sigma.mk i ∘ g)
hi : range (Sigma.mk i ∘ g) ⊆ range (Sigma.mk i)
⊢ ∃ i_1 g_1, Continuous[inst✝², inst✝ i_1] g_1 ∧ Sigma.mk i ∘ g = Sigma.mk i_1 ∘ g_1
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
g : α → X i
hf : Continuous[inst✝², inst✝ i] g
hi : range (Sigma.mk i ∘ g) ⊆ range (Sigma.mk i)
⊢ Continuous[inst✝², inst✝ i] g

Tactic:
]

Goal state after:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
g : α → X i
hf : Continuous[inst✝², inst✝ i] g
hi : range (Sigma.mk i ∘ g) ⊆ range (Sigma.mk i)
⊢ Continuous[inst✝², inst✝ i] g
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen[inst✝] u
huv : Disjoint (frontier u) v
⊢ v ∩ u = v ∩ u

Tactic:
]

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

Goal state before:
pp: α : Type u_2
g : Set (Set α)
f : Filter α
fct : CountableInterFilter f
hf : g ⊆ f.sets
⊢ g ⊆ f.sets

Tactic:
]

Goal state after:
α : Type u_2
g : Set (Set α)
f : Filter α
fct : CountableInterFilter f
hf : g ⊆ f.sets
⊢ g ⊆ f.sets
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
⊢ ¬Nontrivial ι

Tactic:
]

Goal state after:
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
⊢ ¬Nontrivial ι
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_1
α : 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
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
huv : s ⊆ u' ∪ v'
⊢ x ∈ u' ∩ s

Tactic:
]

Goal state after:
case refine_1
α : 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
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
huv : s ⊆ u' ∪ v'
⊢ x ∈ u' ∩ s
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_2
α : 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
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
huv : s ⊆ u' ∪ v'
⊢ y ∈ v' ∩ s

Tactic:
]

Goal state after:
case refine_2
α : 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
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
huv : s ⊆ u' ∪ v'
⊢ y ∈ v' ∩ s
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s j = ∅
hi : s i = univ
⊢ False

Tactic:
]

Goal state after:
case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s j = ∅
hi : s i = univ
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] (⋃ i_1, s i_1 \ s i)

Tactic:
]

Goal state after:
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] (⋃ i_1, s i_1 \ s i)
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
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
huv : s ⊆ u' ∪ v'
z : α
hz : z ∈ f ⁻¹' u ∩ s ∩ (f ⁻¹' v ∩ s)
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
]

Goal state after:
α : 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
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
huv : s ⊆ u' ∪ v'
z : α
hz : z ∈ f ⁻¹' u ∩ s ∩ (f ⁻¹' v ∩ s)
⊢ (f '' s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst✝] t
ht' : IsClosed[inst✝] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
⊢ ¬s ⊆ tᶜ ∪ t'ᶜ

Tactic:
]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst✝] t
ht' : IsClosed[inst✝] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
⊢ ¬s ⊆ tᶜ ∪ t'ᶜ
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsClosed[inst✝²] (⋃ i_1, s i_1 \ s i)

Tactic:
]

Goal state after:
α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsClosed[inst✝²] (⋃ i_1, s i_1 \ s i)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst✝] t
ht' : IsClosed[inst✝] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
xt' : x ∉ t'
yt : y ∉ t
this : (s ∩ (t ∪ t')ᶜ).Nonempty
⊢ False

Tactic:
]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst✝] t
ht' : IsClosed[inst✝] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
xt' : x ∉ t'
yt : y ∉ t
this : (s ∩ (t ∪ t')ᶜ).Nonempty
⊢ False