awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : AccPt y (𝓟 C)
⊢ ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y

Tactic:
rw [accPt_iff_nhds] at this

Premises used: accPt_iff_nhds
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y
rcases : ∀ (x : α) (xC : x ∈ univ ∩ C) (hxy : x ≠ y), ∃ x ∈ C, x ≠ y
⊢ ∃ x ∈ C, x ≠ y

Tactic:
rcases this univ univ_mem with ⟨x, xC, hxy⟩

Premises used: Set.univ, Filter.univ_mem
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y
x : α
xC : x ∈ univ ∩ C
hxy : x ≠ y
⊢ ∃ x ∈ C, x ≠ y

Tactic:
⟨x, xC.2, hxy⟩

Premises used: And.right, And.intro, Exists.intro
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y
x : α
xC : x ∈ univ ∩ C
hxy : x ≠ y
⊢ ∃ x ∈ C, x ≠ y

Tactic:
exact ⟨x, xC.2, hxy⟩
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
obtain :
  ∀ (x : α) (xC : x ∈ C) (hxy : x ≠ y),
    ∃ (C₀ : Set α) (C₁ : Set α),
      (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
⊢ ∃ (C₀ : Set α) (C₁ : Set α),
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁

Tactic:
obtain ⟨x, xC, hxy⟩ : ∃ x ∈ C, x ≠ y := by
    have := hC.acc _ yC
    rw [accPt_iff_nhds] at this
    rcases this univ univ_mem with ⟨x, xC, hxy⟩
    exact ⟨x, xC.2, hxy⟩
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
obtain :
  ∀ (U : Set α) (xU : x ∈ U) (Uop : IsOpen[inst] U) (V : Set α) (yV : y ∈ V) (Vop : IsOpen[inst] V)
    (hUV : Disjoint (closure[inst] U) (closure[inst] V)),
    ∃ (C₀ : Set α) (C₁ : Set α),
      (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
⊢ ∃ (C₀ : Set α) (C₁ : Set α),
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁

Tactic:
obtain ⟨U, xU, Uop, V, yV, Vop, hUV⟩ := exists_open_nhds_disjoint_closure hxy

Premises used: exists_open_nhds_disjoint_closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
h :
  (Perfect (closure[inst] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty ∧ closure[inst] (U ∩ C) ⊆ C) ∧
    (Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty ∧ closure[inst] (V ∩ C) ⊆ C) ∧
      Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))
⊢ ∃ (C₀ : Set α) (C₁ : Set α),
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁

Tactic:
use closure (U ∩ C), closure (V ∩ C)

Premises used: Inter.inter, closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
h : Perfect (closure[inst] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty ∧ closure[inst] (U ∩ C) ⊆ C
h₁ :
  (Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty ∧ closure[inst] (V ∩ C) ⊆ C) ∧
    Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))
⊢ (Perfect (closure[inst] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty ∧ closure[inst] (U ∩ C) ⊆ C) ∧
    (Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty ∧ closure[inst] (V ∩ C) ⊆ C) ∧
      Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))

Tactic:
constructor
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
h : (Perfect (closure[inst] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty) ∧ closure[inst] (U ∩ C) ⊆ C
⊢ Perfect (closure[inst] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty ∧ closure[inst] (U ∩ C) ⊆ C

Tactic:
rw [← and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
h :
  ((Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty) ∧ closure[inst] (V ∩ C) ⊆ C) ∧
    Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))
⊢ (Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty ∧ closure[inst] (V ∩ C) ⊆ C) ∧
    Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))

Tactic:
rw [← and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
⊢ (Perfect (closure[inst] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty) ∧ closure[inst] (U ∩ C) ⊆ C

Tactic:
⟨hC.closure_nhds_inter x xC xU Uop, ?_⟩

Premises used: Perfect.closure_nhds_inter, And.intro
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
h : closure[inst] (U ∩ C) ⊆ C
⊢ (Perfect (closure[inst] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty) ∧ closure[inst] (U ∩ C) ⊆ C

Tactic:
refine ⟨hC.closure_nhds_inter x xC xU Uop, ?_⟩
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
h : U ∩ C ⊆ C
⊢ closure[inst] (U ∩ C) ⊆ C

Tactic:
rw [hC.closed.closure_subset_iff]

Premises used: Perfect.closed, IsClosed.closure_subset_iff
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
⊢ U ∩ C ⊆ C

Tactic:
inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
⊢ U ∩ C ⊆ C

Tactic:
exact inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
h : (Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty) ∧ closure[inst] (V ∩ C) ⊆ C
h₁ : Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))
⊢ ((Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty) ∧ closure[inst] (V ∩ C) ⊆ C) ∧
    Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))

Tactic:
constructor
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
⊢ (Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty) ∧ closure[inst] (V ∩ C) ⊆ C

Tactic:
⟨hC.closure_nhds_inter y yC yV Vop, ?_⟩

Premises used: Perfect.closure_nhds_inter, And.intro
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
h : closure[inst] (V ∩ C) ⊆ C
⊢ (Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty) ∧ closure[inst] (V ∩ C) ⊆ C

Tactic:
refine ⟨hC.closure_nhds_inter y yC yV Vop, ?_⟩
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
h : V ∩ C ⊆ C
⊢ closure[inst] (V ∩ C) ⊆ C

Tactic:
rw [hC.closed.closure_subset_iff]

Premises used: Perfect.closed, IsClosed.closure_subset_iff
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
⊢ V ∩ C ⊆ C

Tactic:
inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
⊢ V ∩ C ⊆ C

Tactic:
exact inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
apply : closure[inst] (U ∩ C) ≤ closure[inst] U
apply₁ : closure[inst] (V ∩ C) ≤ closure[inst] V
⊢ Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))

Tactic:
apply Disjoint.mono _ _ hUV

Premises used: Disjoint.mono
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
h : U ∩ C ⊆ U
⊢ closure[inst] (U ∩ C) ≤ closure[inst] U

Tactic:
apply closure_mono

Premises used: closure_mono
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
h : V ∩ C ⊆ V
⊢ closure[inst] (V ∩ C) ≤ closure[inst] V

Tactic:
apply closure_mono

Premises used: closure_mono
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
⊢ U ∩ C ⊆ U

Tactic:
inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
⊢ U ∩ C ⊆ U

Tactic:
exact inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
⊢ V ∩ C ⊆ V

Tactic:
inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst] V
hUV : Disjoint (closure[inst] U) (closure[inst] V)
⊢ V ∩ C ⊆ V

Tactic:
exact inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h : IsPreconnected U
x : α
hx : x ∈ U
rw :
  ∀
    (h :
      ∀ (t t' : Set α),
        IsClosed[inst] t →
          IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty)
    (x : α) (hx : x ∈ U), AccPt x (𝓟 U)
⊢ AccPt x (𝓟 U)

Tactic:
rw [isPreconnected_closed_iff] at h

Premises used: isPreconnected_closed_iff
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
specialize_1 : U ⊆ {x} ∪ closure[inst] (U \ {x})
specialize_2 : (U ∩ {x}).Nonempty
specialize_3 : (U ∩ closure[inst] (U \ {x})).Nonempty
specialize : ∀ (h : (U ∩ ({x} ∩ closure[inst] (U \ {x}))).Nonempty), AccPt x (𝓟 U)
⊢ AccPt x (𝓟 U)

Tactic:
specialize h {x} (closure (U \ {x})) isClosed_singleton isClosed_closure ?_ ?_ ?_

Premises used: SDiff.sdiff, closure, Singleton.singleton, isClosed_closure, isClosed_singleton
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
trans : U ⊆ {x} ∪ U \ {x}
trans₁ : {x} ∪ U \ {x} ⊆ {x} ∪ closure[inst] (U \ {x})
⊢ U ⊆ {x} ∪ closure[inst] (U \ {x})

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

Premises used: SDiff.sdiff, Singleton.singleton
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ U ⊆ {x} ∪ U \ {x}

Tactic:
simp
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
h₁ : U \ {x} ⊆ closure[inst] (U \ {x})
⊢ {x} ∪ U \ {x} ⊆ {x} ∪ closure[inst] (U \ {x})

Tactic:
apply Set.union_subset_union_right

Premises used: Set.union_subset_union_right
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ U \ {x} ⊆ closure[inst] (U \ {x})

Tactic:
subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ U \ {x} ⊆ closure[inst] (U \ {x})

Tactic:
exact subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ (U ∩ {x}).Nonempty

Tactic:
Set.inter_singleton_nonempty.mpr hx

Premises used: Iff.mpr, Set.inter_singleton_nonempty
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] 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

Premises used: Iff.mpr, Set.inter_singleton_nonempty
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
specialize_3 : ∀ (y : α) (hy : y ∈ U ∧ y ≠ x), (U ∩ closure[inst] (U \ {x})).Nonempty
⊢ (U ∩ closure[inst] (U \ {x})).Nonempty

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

Premises used: Set.Nontrivial.exists_ne
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
y : α
hy : y ∈ U ∧ y ≠ x
h₁ : y ∈ U ∩ closure[inst] (U \ {x})
⊢ (U ∩ closure[inst] (U \ {x})).Nonempty

Tactic:
use y
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
y : α
hy : y ∈ U ∧ y ≠ x
h₁ : y ∈ closure[inst] (U \ {x})
⊢ y ∈ U ∩ closure[inst] (U \ {x})

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

Premises used: Set.mem_inter_iff, true_and
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
y : α
hy : y ∈ U ∧ y ≠ x
h₁ : y ∈ U \ {x}
⊢ y ∈ closure[inst] (U \ {x})

Tactic:
apply subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] 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]
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : (U ∩ ({x} ∩ closure[inst] (U \ {x}))).Nonempty
⊢ ({x} ∩ closure[inst] (U \ {x})).Nonempty

Tactic:
apply Set.Nonempty.right at h

Premises used: Set.Nonempty.right
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : ({x} ∩ closure[inst] (U \ {x})).Nonempty
⊢ AccPt x (𝓟 U)

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

Premises used: mem_closure_iff_clusterPt, accPt_principal_iff_clusterPt, Set.singleton_inter_nonempty
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : AccPt x (𝓟 U)
⊢ AccPt x (𝓟 U)

Tactic:
h
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : AccPt x (𝓟 U)
⊢ AccPt x (𝓟 U)

Tactic:
exact h
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
inst_2 : ConnectedSpace α
inst_3 : Nontrivial α
univ_preperfect : Preperfect.{u_1} (α := α) univ
⊢ PerfectSpace α

Tactic:
constructor
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
inst_2 : ConnectedSpace α
inst_3 : Nontrivial α
univ_preperfect : Set.Nontrivial.{u_1} (α := α) univ
⊢ Preperfect.{u_1} (α := α) univ

Tactic:
apply isPreconnected_univ.preperfect_of_nontrivial

Premises used: PreconnectedSpace.isPreconnected_univ, IsPreconnected.preperfect_of_nontrivial
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
inst_2 : ConnectedSpace α
inst_3 univ_preperfect : Nontrivial α
⊢ Set.Nontrivial.{u_1} (α := α) univ

Tactic:
rw [Set.nontrivial_univ_iff]

Premises used: Set.nontrivial_univ_iff
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
inst_2 : ConnectedSpace α
inst_3 : Nontrivial α
⊢ Nontrivial α

Tactic:
infer_instance
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
obtain :
  ∀ (b : Set (Set α)) (bct : b.Countable),
    ∅ ∉ b → ∀ (bbasis : IsTopologicalBasis b), ∃ (V : Set α) (D : Set α), V.Countable ∧ Perfect D ∧ C = V ∪ D
⊢ ∃ (V : Set α) (D : Set α), V.Countable ∧ Perfect D ∧ C = V ∪ D

Tactic:
obtain ⟨b, bct, _, bbasis⟩ := TopologicalSpace.exists_countable_basis α

Premises used: TopologicalSpace.exists_countable_basis
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
b : Set (Set α)
bct : b.Countable
left : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U : Set α | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
simp : Set.Countable.{u_1} (α := α) (⋃ i ∈ v, i ∩ C)
⊢ (V ∩ C).Countable

Tactic:
simp only [V, iUnion_inter]

Premises used: Set.iUnion_inter
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
b : Set (Set α)
bct : b.Countable
left : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U : Set α | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
hs : v.Countable
a : ∀ (a : Set α) (ha : a ∈ v), (a ∩ C).Countable
⊢ Set.Countable.{u_1} (α := α) (⋃ i ∈ v, i ∩ C)

Tactic:
apply Countable.biUnion

Premises used: Set.Countable.biUnion
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
b : Set (Set α)
bct : b.Countable
left : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U : Set α | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
⊢ v.Countable

Tactic:
bct.mono (sep_subset _ _)

Premises used: Set.Countable.mono, Set.sep_subset
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
b : Set (Set α)
bct : b.Countable
left : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U : Set α | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
⊢ v.Countable

Tactic:
exact bct.mono (sep_subset _ _)

Premises used: Set.Countable.mono, Set.sep_subset