mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ sᶜ

pp: case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ ∅

pp: case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ sᶜ

pp: case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ ∅

pp: case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ sᶜ

pp: case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ ∅

pp: case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ sᶜ

pp: case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ ∅

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ sᶜ

case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ ∅

case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ sᶜ

case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ ∅

case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ sᶜ

case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ ∅

case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ sᶜ

case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ ∅
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ s ∪ sᶜ = univ ∨ s ∪ sᶜ = s ∨ s ∪ sᶜ = sᶜ ∨ s ∪ sᶜ = ∅

pp: case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ s ∪ ∅ = univ ∨ s ∪ ∅ = s ∨ s ∪ ∅ = sᶜ ∨ s ∪ ∅ = ∅

pp: case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ ∅ ∪ sᶜ = univ ∨ ∅ ∪ sᶜ = s ∨ ∅ ∪ sᶜ = sᶜ ∨ ∅ ∪ sᶜ = ∅

pp: case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ ∅ ∪ ∅ = univ ∨ ∅ ∪ ∅ = s ∨ ∅ ∪ ∅ = sᶜ ∨ ∅ ∪ ∅ = ∅

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ s ∪ sᶜ = univ ∨ s ∪ sᶜ = s ∨ s ∪ sᶜ = sᶜ ∨ s ∪ sᶜ = ∅

case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ s ∪ ∅ = univ ∨ s ∪ ∅ = s ∨ s ∪ ∅ = sᶜ ∨ s ∪ ∅ = ∅

case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ ∅ ∪ sᶜ = univ ∨ ∅ ∪ sᶜ = s ∨ ∅ ∪ sᶜ = sᶜ ∨ ∅ ∪ sᶜ = ∅

case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ ∅ ∪ ∅ = univ ∨ ∅ ∪ ∅ = s ∨ ∅ ∪ ∅ = sᶜ ∨ ∅ ∪ ∅ = ∅
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inl
α : Type u
inst✝ : TopologicalSpace α
x : α
t : Set α
H2 : x ∈ t
H4 : IsPreconnected t
r : Set α
H1 : x ∈ r
H3 : IsPreconnected r
⊢ x ∈ r

pp: case inr
α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ x ∈ t

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝ : TopologicalSpace α
x : α
t : Set α
H2 : x ∈ t
H4 : IsPreconnected t
r : Set α
H1 : x ∈ r
H3 : IsPreconnected r
⊢ x ∈ r

case inr
α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ x ∈ t
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inl
α : Type u
inst✝ : TopologicalSpace α
x : α
t : Set α
H2 : x ∈ t
H4 : IsPreconnected t
r : Set α
H1 : x ∈ r
H3 : IsPreconnected r
⊢ IsPreconnected r

pp: case inr
α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ IsPreconnected t

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝ : TopologicalSpace α
x : α
t : Set α
H2 : x ∈ t
H4 : IsPreconnected t
r : Set α
H1 : x ∈ r
H3 : IsPreconnected r
⊢ IsPreconnected r

case inr
α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ IsPreconnected t
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mpr.refine_1
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ x ∈ interior U

pp: case mpr.refine_2
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ x ∈ interior U

pp: case mpr.refine_3
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ x ∈ interior U

Tactic:
<;>

Goal state after:
case mpr.refine_1
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ x ∈ interior U

case mpr.refine_2
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ x ∈ interior U

case mpr.refine_3
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ x ∈ interior U
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case h₁
ι : 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 ⊆ s i hi

pp: case h₂
ι : 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), t i h ⊆ t i hi

Tactic:
<;>

Goal state after:
case h₁
ι : 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 ⊆ s i hi

case h₂
ι : 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), t i h ⊆ 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₁

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

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 ∈ l₁

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₂
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mp
α : Type u_2
g : Set (Set α)
s : Set α
⊢ s ∈ countableGenerate g → ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

pp: case mpr
α : Type u_2
g : Set (Set α)
s : Set α
⊢ (∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s) → s ∈ countableGenerate g

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
g : Set (Set α)
s : Set α
⊢ s ∈ countableGenerate g → ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

case mpr
α : Type u_2
g : Set (Set α)
s : Set α
⊢ (∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s) → s ∈ countableGenerate g
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mp
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ f ≤ countableGenerate g → g ⊆ f.sets

pp: case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ g ⊆ f.sets → f ≤ countableGenerate g

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ f ≤ countableGenerate g → g ⊆ f.sets

case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ g ⊆ f.sets → f ≤ countableGenerate g
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)
i j : ι
h_ne : i ≠ j
⊢ s i ∩ s j = ∅

Tactic:
simpa only [← bot_eq_empty, eq_bot_iff, ← inf_eq_inter, ← disjoint_iff_inf_le] using h_disj h_ne

Goal state after:
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 ∈ s ∩ u'

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 ∈ s ∩ v'

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 ∈ s ∩ u'

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 ∈ s ∩ v'
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen[inst✝] u
hu' : IsOpen[inst✝¹] (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen[inst✝] v
hv' : IsOpen[inst✝¹] (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty

Tactic:
replace huv : f '' s ⊆ u ∪ v := by rwa [image_subset_iff]

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen[inst✝] u
hu' : IsOpen[inst✝¹] (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen[inst✝] v
hv' : IsOpen[inst✝¹] (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : f '' s ⊆ u ∪ v
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsPreconnected s → ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ (∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) → IsPreconnected s

Tactic:
<;>

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsPreconnected s → ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ (∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) → IsPreconnected s
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsPreconnected s →
    ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ (∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) →
    IsPreconnected s

Tactic:
<;>

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsPreconnected s →
    ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ (∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) →
    IsPreconnected s
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case inr
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
f : ℕ → ↑c
f_surj : Function.Surjective f
x : ι
hx : x ∈ c
n : ℕ
hn : f n = ⟨x, hx⟩
⊢ U x ⊆ ⋃ n, U ↑(f n)

Tactic:
exact subset_iUnion_of_subset n <| subset_of_eq (by rw [hn])

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

Goal state before:
pp: case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
⊢ (∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
⊢ (∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
⊢ (∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
⊢ (∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case pos
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∈ F
⊢ (Subtype.val '' connectedComponent ⟨x, h✝⟩).Nonempty ↔ x ∈ F

pp: case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∉ F
⊢ ∅.Nonempty ↔ x ∈ F

Tactic:
<;>

Goal state after:
case pos
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∈ F
⊢ (Subtype.val '' connectedComponent ⟨x, h✝⟩).Nonempty ↔ x ∈ F

case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∉ F
⊢ ∅.Nonempty ↔ x ∈ F
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case pos
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
h✝ : x ∈ F
⊢ Subtype.val '' connectedComponent ⟨x, h✝⟩ ⊆ F

pp: case neg
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
h✝ : x ∉ F
⊢ ∅ ⊆ F

Tactic:
<;>

Goal state after:
case pos
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
h✝ : x ∈ F
⊢ Subtype.val '' connectedComponent ⟨x, h✝⟩ ⊆ F

case neg
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
h✝ : x ∉ F
⊢ ∅ ⊆ F
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
⊢ T3Space X → T0Space X

pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
⊢ T0Space X → T3Space X

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
⊢ T3Space X → T0Space X

case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
⊢ T0Space X → T3Space X
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
a✝ : T3Space X
⊢ T0Space X

pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
a✝ : T0Space X
⊢ T3Space X

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
a✝ : T3Space X
⊢ T0Space X

case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
a✝ : T0Space X
⊢ T3Space X
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
F : Set β
hf : ContinuousOn f (f ⁻¹' F)
y : β
⊢ f ⁻¹' connectedComponentIn F y = ⋃ x ∈ f ⁻¹' connectedComponentIn F y, connectedComponentIn (f ⁻¹' F) x

Tactic:
refine subset_antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun x hx z hz ↦ ?_)

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
F : Set β
hf : ContinuousOn f (f ⁻¹' F)
y : β
z : α
hz : z ∈ f ⁻¹' connectedComponentIn F y
⊢ z ∈ ⋃ x ∈ f ⁻¹' connectedComponentIn F y, connectedComponentIn (f ⁻¹' F) x

case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
F : Set β
hf : ContinuousOn f (f ⁻¹' F)
y : β
x : α
hx : x ∈ f ⁻¹' connectedComponentIn F y
z : α
hz : z ∈ connectedComponentIn (f ⁻¹' F) x
⊢ z ∈ f ⁻¹' connectedComponentIn F y
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case false
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (bif false then s else t)

pp: case true
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (bif true then s else t)

Tactic:
<;>

Goal state after:
case false
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (bif false then s else t)

case true
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (bif true then s else t)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected univ

Tactic:
by rw [univ_eq_empty_iff.mpr hα]; exact isPreconnected_empty

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ closure[inst✝¹] s

Tactic:
di.isInducing.closure_eq_preimage_closure_image,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ i ⁻¹' closure[inst✝] (i '' s)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
⊢ di.extend f (i a) = f a

Tactic:
rcases hf (i a) with ⟨b, hb⟩
  refine di.extend_eq_at' b ?_
  rwa [← di.isInducing.nhds_eq_comap] at hb

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

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

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

Tactic:
<;>

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

case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (SeparationQuotient.mk ⁻¹' s) (closure[inst✝²] (SeparationQuotient.mk ⁻¹' t))
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: case refine_1
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst✝¹] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ ∀ s ∈ f '' S, IsOpen[inst✝¹] s

pp: case refine_2
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst✝¹] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ ∀ s ∈ f '' S, Dense s

Tactic:
<;>

Goal state after:
case refine_1
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst✝¹] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ ∀ s ∈ f '' S, IsOpen[inst✝¹] s

case refine_2
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst✝¹] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ ∀ s ∈ f '' S, Dense s