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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x✝ : X
hx : x✝ ∈ S
hx'✝ : x✝ ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
x : X
hx' : x ∈ ⋂₀ ↑{U, u, v}
⊢ x ∈ U ∧ x ∈ u ∧ x ∈ v

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x✝ : X
hx : x✝ ∈ S
hx'✝ : x✝ ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
x : X
hx' : x ∈ ⋂₀ ↑{U, u, v}
⊢ x ∈ U ∧ x ∈ u ∧ x ∈ v
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
i✝ : T2Quotient X
x : X
j✝ : T2Quotient X
y : X
h : ¬mk x = mk y
⊢ ∃ s, T2Space (Quotient s) ∧ ⟦x⟧ ≠ ⟦y⟧

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
i✝ : T2Quotient X
x : X
j✝ : T2Quotient X
y : X
h : ¬mk x = mk y
⊢ ∃ s, T2Space (Quotient s) ∧ ¬s x y
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case empty
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
⊢ Dense (s \ ↑∅)

Tactic:
simpa using

Goal state after:
case empty
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
⊢ Dense s
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
t : Set X
h₁t : t ∈ 𝓝[s] p
h₂t : t.Finite
S : Set X := {y | y ∈ t ∩ s ∧ ¬y ⤳ p}
y : X
hy : y ∈ S
⊢ p ∈ (closure[inst✝] {y})ᶜ

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
t : Set X
h₁t : t ∈ 𝓝[s] p
h₂t : t.Finite
S : Set X := {y | y ∈ t ∩ s ∧ ¬y ⤳ p}
y : X
hy : y ∈ S
⊢ p ∉ closure[inst✝] {y}
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case a
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ 𝓝[s] p ≤ 𝓟 ({x | x ⤳ p} ∩ s)

Tactic:
simpa using

Goal state after:
case a
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ {x | x ⤳ p} ∈ 𝓝[s] p ∧ s ∈ 𝓝[s] p
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst✝¹] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ {x} ∈ 𝓝 x

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst✝¹] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ {x} ∈ 𝓝 x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case h₁
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ ∀ V ∈ 𝓝 p, {x | x ⤳ p} ⊆ V

Tactic:
exact fun s hs x hx ↦ mem_of_mem_nhds (hx hs)

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : DiscreteTopology ↑s
x : X
hx : x ∈ s
this : {⟨x, hx⟩} ∈ 𝓝 ⟨x, hx⟩
⊢ {x} ∈ 𝓝[s] x

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : DiscreteTopology ↑s
x : X
hx : x ∈ s
this : {⟨x, hx⟩} ∈ 𝓝 ⟨x, hx⟩
⊢ {x} ∈ map Subtype.val (𝓝 ⟨x, hx⟩)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
⊢ ∃ U ∈ 𝓝 x, U ∩ s = {x}

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
⊢ ∃ U ∈ 𝓝 x, U ∩ s = {x}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case empty
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ i ∈ ∅, IsOpen[inst✝¹] (U i)
hsC : s ⊆ ⋃ i ∈ ∅, U i
⊢ s = ⋃ i ∈ ∅, (fun x ↦ ∅) i

Tactic:
simpa using

Goal state after:
case empty
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ i ∈ ∅, IsOpen[inst✝¹] (U i)
hsC : s ⊆ ⋃ i ∈ ∅, U i
⊢ s = ∅
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a b : α
H : a < b
⊢ Ioo a b ∈ 𝓝[<] b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a b : α
H : a < b
⊢ Iio b ∩ Ioi a ∈ 𝓝[<] b
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClopen s
ht : IsClopen t
⊢ IsClopen (s ⇨ t)

Tactic:
simpa using

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClopen s
ht : IsClopen t
⊢ IsClopen (t ∪ sᶜ)
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
this : IsClosed[inst✝] (s ∩ bᶜ)
x : X
hx₁ : x ∈ s
hx₂ : x ∈ bᶜ
⊢ x ∈ a

Tactic:
simpa using

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
this : IsClosed[inst✝] (s ∩ bᶜ)
x : X
hx₁ : x ∈ s
hx₂ : x ∈ bᶜ
⊢ x ∈ a
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:
simpa using

Goal state after:
α : 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}
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: case refine_1
α : 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
⊢ ContinuousOn f' (closure[inst✝²] {x | f x ≤ g x})

pp: case refine_2
α : 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
⊢ closure[inst✝²] {x | ¬f x ≤ g x} ⊆ {x | g x ≤ f x}

Tactic:
· rwa [(isClosed_le hf hg).closure_eq]

Goal state after:
case refine_2
α : 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
⊢ closure[inst✝²] {x | ¬f x ≤ g x} ⊆ {x | g x ≤ f x}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case pos
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ∃ t ∈ T, Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

pp: case neg
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ∀ t ∈ T, ¬Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
· rcases hTd with ⟨t, htT, htd⟩
    exact .inr <| htd.mono (iInf₂_le t htT) (iInf₂_le t htT)

Goal state after:
case neg
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ∀ t ∈ T, ¬Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: case refine_2
α : 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
⊢ closure[inst✝²] {x | ¬f x ≤ g x} ⊆ {x | g x ≤ f x}

Tactic:
simp only [not_le]

Goal state after:
case refine_2
α : 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
⊢ closure[inst✝²] {x | g x < f x} ⊆ {x | g x ≤ f x}
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)
y : Y
hys : y ∉ interior s
hxy : Inseparable (f x) y
⊢ f x ∈ interior s

Tactic:
rwa [mem_interior_iff_mem_nhds]

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:
simpa using

Goal state after:
α : 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)
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:
simpa using

Goal state after:
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)
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:
simpa using

Goal state after:
ι : Sort u_1
α : Type u_2
l : Filter α
inst✝¹ : CountableInterFilter l
inst✝ : Countable ι
p : α → ι → Prop
⊢ ⋂ i, {x | p x i} ∈ l ↔ ∀ (i : ι), {x | p x i} ∈ l
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:
simpa using

Goal state after:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
p : α → (i : ι) → i ∈ S → Prop
⊢ ⋂ i, ⋂ (i_1 : i ∈ S), {x | p x i i_1} ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), {x | p x i hi} ∈ l
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:
← biUnion_univ

Goal state after:
α : 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 (⋃ x ∈ univ, s x)
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:
simpa using

Goal state after:
α : 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 j
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:
refine locallyConnectedSpace_iff_connected_subsets.2 fun x U hU ↦ ?_

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 : U ∈ 𝓝 x
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
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 : α → β
S : Set (Set α)
hSc : S.Countable
t : Set α → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
this : ⋂ s ∈ S, t s ∈ l
⊢ f ⁻¹' ⋂ s ∈ S, t s ⊆ ⋂₀ S

Tactic:
simpa using

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
t : Set α → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
this : ⋂ s ∈ S, t s ∈ l
⊢ ∀ t' ∈ S, ⋂ i ∈ S, f ⁻¹' t i ⊆ t'
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s t : Set α
⊢ IsOpen[inst✝¹] s → IsOpen[inst✝¹] t → s ∪ t = univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

Tactic:
simpa using

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s t : Set α
⊢ IsOpen[inst✝¹] s → IsOpen[inst✝¹] t → s ∪ t = univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : Set α
hs : IsClopen s
h : ¬(s = ∅ ∨ s = univ)
⊢ s.Nonempty ∧ sᶜ.Nonempty

Tactic:
simpa using

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : Set α
hs : IsClopen s
h : ¬(s = ∅ ∨ s = univ)
⊢ ¬s = ∅ ∧ ¬s = univ
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 using

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)
i j : ι
h_ne : i ≠ j
⊢ Disjoint (s i) (s j)
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_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsOpen[inst✝¹] (s j \ s i)

Tactic:
simpa using

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_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsOpen[inst✝¹] (s j)
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)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsClosed[inst✝²] (s j \ s i)

Tactic:
simpa using

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)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsClosed[inst✝²] (s j)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
a : α
ha : P z a
h'a : a ∈ s
⊢ P z a ∧ P a z

Tactic:
exact ⟨ha, h'' z a hz h'a ha⟩

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ s ⊆ f '' u ∪ f '' v

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ s ⊆ f '' u ∪ f '' v
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty

Tactic:
simpa using

Goal state after:
case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x✝ : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hU : ∀ (u v : Set α), u ∈ ∅ → v ∈ ∅ → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ ∅, IsOpen[inst✝] u
hsU : s ⊆ ⋃₀ ↑∅
⊢ s ⊆ ∅

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x✝ : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hU : ∀ (u v : Set α), u ∈ ∅ → v ∈ ∅ → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ ∅, IsOpen[inst✝] u
hsU : s ⊆ ⋃₀ ↑∅
⊢ s = ∅
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ s ⊆ f '' u ∪ f '' v

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ s ⊆ f '' u ∪ f '' v
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty

Tactic:
simpa using

Goal state after:
case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
⊢ s.Nonempty

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
⊢ ¬s = ∅