-- Mathlib/Topology/Perfect.lean
lemma IsPreconnected.preperfect_of_nontrivial [T1Space α] {U : Set α} (hu : U.Nontrivial)
    (h : IsPreconnected U) : Preperfect U

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : AccPt x (𝓟 U)
⊢ AccPt x (𝓟 U)

Tactic:
exact h

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
y : α
hy : y ∈ U ∧ y ≠ x
⊢ y ∈ U ∩ closure (U \ {x})

Tactic:
simp only [Set.mem_inter_iff, hy, true_and]

Result:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
y : α
hy : y ∈ U ∧ y ≠ x
⊢ y ∈ closure (U \ {x})

Proof state:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
y : α
hy : y ∈ U ∧ y ≠ x
⊢ y ∈ closure (U \ {x})

Tactic:
apply subset_closure

Result:
case h.a
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
y : α
hy : y ∈ U ∧ y ≠ x
⊢ y ∈ U \ {x}

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ {x} ∪ U \ {x} ⊆ {x} ∪ closure (U \ {x})

Tactic:
apply Set.union_subset_union_right

Result:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ U \ {x} ⊆ closure (U \ {x})

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : ({x} ∩ closure (U \ {x})).Nonempty
⊢ AccPt x (𝓟 U)

Tactic:
rw [Set.singleton_inter_nonempty, mem_closure_iff_clusterPt, ← acc_principal_iff_cluster] at h

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : AccPt x (𝓟 U)
⊢ AccPt x (𝓟 U)

Proof state:
case specialize_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ (U ∩ closure (U \ {x})).Nonempty

Tactic:
obtain ⟨y, hy⟩ := Set.Nontrivial.exists_ne hu x

Result:
case specialize_3.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
y : α
hy : y ∈ U ∧ y ≠ x
⊢ (U ∩ closure (U \ {x})).Nonempty

Proof state:
case specialize_3.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
y : α
hy : y ∈ U ∧ y ≠ x
⊢ (U ∩ closure (U \ {x})).Nonempty

Tactic:
use y

Result:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
y : α
hy : y ∈ U ∧ y ≠ x
⊢ y ∈ U ∩ closure (U \ {x})

Proof state:
case specialize_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ U ⊆ {x} ∪ closure (U \ {x})

Tactic:
trans {x} ∪ (U \ {x})

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ U ⊆ {x} ∪ U \ {x}

α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ {x} ∪ U \ {x} ⊆ {x} ∪ closure (U \ {x})

Proof state:
case h.a
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
y : α
hy : y ∈ U ∧ y ≠ x
⊢ y ∈ U \ {x}

Tactic:
simp [hy]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : (U ∩ ({x} ∩ closure (U \ {x}))).Nonempty
⊢ AccPt x (𝓟 U)

Tactic:
apply Set.Nonempty.right at h

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : ({x} ∩ closure (U \ {x})).Nonempty
⊢ AccPt x (𝓟 U)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h : IsPreconnected U
x : α
hx : x ∈ U
⊢ AccPt x (𝓟 U)

Tactic:
rw [isPreconnected_closed_iff] at h

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ AccPt x (𝓟 U)

Proof state:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ U \ {x} ⊆ closure (U \ {x})

Tactic:
exact subset_closure

Result:
no goals

Proof state:
case specialize_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ (U ∩ {x}).Nonempty

Tactic:
exact Set.inter_singleton_nonempty.mpr hx

Result:
no goals