awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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) ∧
    (Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty ∧ closure[inst] (V ∩ C) ⊆ C) ∧
      Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
have h : (Perfect (closure[inst] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty) ∧ closure[inst] (U ∩ C) ⊆ C
Tactic: rw [← and_assoc]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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) ∧
    Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))
have 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))
Tactic: rw [← and_assoc]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
have h : closure[inst] (U ∩ C) ⊆ C
Tactic: refine ⟨hC.closure_nhds_inter x xC xU Uop, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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)
⊢ closure[inst] (U ∩ C) ⊆ C
have h : U ∩ C ⊆ C
Tactic: rw [hC.closed.closure_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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) ∧
    Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))
have h : (Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty) ∧ closure[inst] (V ∩ C) ⊆ C
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
⊢ ((Perfect (closure[inst] (V ∩ C)) ∧ (closure[inst] (V ∩ C)).Nonempty) ∧ closure[inst] (V ∩ C) ⊆ C) ∧
    Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))
have h₁ : Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
have h : closure[inst] (V ∩ C) ⊆ C
Tactic: refine ⟨hC.closure_nhds_inter y yC yV Vop, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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)
⊢ closure[inst] (V ∩ C) ⊆ C
have h : V ∩ C ⊆ C
Tactic: rw [hC.closed.closure_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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)
⊢ Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))
have apply : closure[inst] (U ∩ C) ≤ closure[inst] U
Tactic: apply Disjoint.mono _ _ hUV
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
⊢ Disjoint (closure[inst] (U ∩ C)) (closure[inst] (V ∩ C))
have apply₁ : closure[inst] (V ∩ C) ≤ closure[inst] V
Tactic: apply Disjoint.mono _ _ hUV
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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)
⊢ closure[inst] (U ∩ C) ≤ closure[inst] U
have h : U ∩ C ⊆ U
Tactic: apply closure_mono
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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)
⊢ closure[inst] (V ∩ C) ≤ closure[inst] V
have h : V ∩ C ⊆ V
Tactic: apply closure_mono
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T1Space α
U : Set α
hu : U.Nontrivial
h : IsPreconnected U
x : α
hx : x ∈ U
⊢ AccPt x (𝓟 U)
have 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)
Tactic: rw [isPreconnected_closed_iff] at h
Cleared hypotheses: h, x, hx
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
⊢ AccPt x (𝓟 U)
have specialize_1 : U ⊆ {x} ∪ closure[inst] (U \ {x})
Tactic: specialize h {x} (closure (U \ {x})) isClosed_singleton isClosed_closure ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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})
⊢ AccPt x (𝓟 U)
have specialize_2 : (U ∩ {x}).Nonempty
Tactic: specialize h {x} (closure (U \ {x})) isClosed_singleton isClosed_closure ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
⊢ AccPt x (𝓟 U)
have specialize_3 : (U ∩ closure[inst] (U \ {x})).Nonempty
Tactic: specialize h {x} (closure (U \ {x})) isClosed_singleton isClosed_closure ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
⊢ AccPt x (𝓟 U)
have specialize : ∀ (h : (U ∩ ({x} ∩ closure[inst] (U \ {x}))).Nonempty), AccPt x (𝓟 U)
Tactic: specialize h {x} (closure (U \ {x})) isClosed_singleton isClosed_closure ?_ ?_ ?_
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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})
have trans : U ⊆ {x} ∪ U \ {x}
Tactic: trans {x} ∪ (U \ {x})
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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}
⊢ U ⊆ {x} ∪ closure[inst] (U \ {x})
have trans₁ : {x} ∪ U \ {x} ⊆ {x} ∪ closure[inst] (U \ {x})
Tactic: trans {x} ∪ (U \ {x})
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
⊢ {x} ∪ U \ {x} ⊆ {x} ∪ closure[inst] (U \ {x})
have h₁ : U \ {x} ⊆ closure[inst] (U \ {x})
Tactic: apply Set.union_subset_union_right
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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 ∩ closure[inst] (U \ {x})).Nonempty
have specialize_3 : ∀ (y : α) (hy : y ∈ U ∧ y ≠ x), (U ∩ closure[inst] (U \ {x})).Nonempty
Tactic: obtain ⟨y, hy⟩ := Set.Nontrivial.exists_ne hu x
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
⊢ (U ∩ closure[inst] (U \ {x})).Nonempty
have h₁ : y ∈ U ∩ closure[inst] (U \ {x})
Tactic: use y
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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 ∩ closure[inst] (U \ {x})
have h₁ : y ∈ closure[inst] (U \ {x})
Tactic: simp only [Set.mem_inter_iff, hy, true_and]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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 ∈ closure[inst] (U \ {x})
have h₁ : y ∈ U \ {x}
Tactic: apply subset_closure
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
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
⊢ AccPt x (𝓟 U)
have h₁ : ({x} ∩ closure[inst] (U \ {x})).Nonempty
Tactic: apply Set.Nonempty.right at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
inst_2 : ConnectedSpace α
inst_3 : Nontrivial α
⊢ PerfectSpace α
have univ_preperfect : Preperfect.{u_1} (α := α) univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
inst_2 : ConnectedSpace α
inst_3 : Nontrivial α
⊢ Preperfect.{u_1} (α := α) univ
have univ_preperfect : Set.Nontrivial.{u_1} (α := α) univ
Tactic: apply isPreconnected_univ.preperfect_of_nontrivial
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
⊢ ∃ (V : Set α) (D : Set α), V.Countable ∧ Perfect D ∧ C = V ∪ D
have obtain : ∀ (b : Set (Set α)) (bct : b.Countable),
  ∅ ∉ b → ∀ (bbasis : IsTopologicalBasis b), ∃ (V : Set α) (D : Set α), V.Countable ∧ Perfect D ∧ C = V ∪ D
Tactic: obtain ⟨b, bct, _, bbasis⟩ := TopologicalSpace.exists_countable_basis α
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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 ∩ C).Countable
have simp : Set.Countable.{u_1} (α := α) (⋃ i ∈ v, i ∩ C)
Tactic: simp only [V, iUnion_inter]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
⊢ Set.Countable.{u_1} (α := α) (⋃ i ∈ v, i ∩ C)
have hs : v.Countable
Tactic: apply Countable.biUnion
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
⊢ Set.Countable.{u_1} (α := α) (⋃ i ∈ v, i ∩ C)
have a : ∀ (a : Set α) (ha : a ∈ v), (a ∩ C).Countable
Tactic: apply Countable.biUnion
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
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 : Set α) (D : Set α), V.Countable ∧ Perfect D ∧ C = V ∪ D
have Vct : (V ∩ C).Countable
Tactic: have Vct : (V ∩ C).Countable := by
    simp only [V, iUnion_inter]
    apply Countable.biUnion
    · exact bct.mono (sep_subset _ _)
    · exact sep_subset_setOf _ _
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
Vct : (V ∩ C).Countable
⊢ ∃ (V : Set α) (D : Set α), V.Countable ∧ Perfect D ∧ C = V ∪ D
have refine_1 : IsClosed[inst] D
Tactic: refine ⟨V ∩ C, D, Vct, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
Vct : (V ∩ C).Countable
refine_1 : IsClosed[inst] D
⊢ ∃ (V : Set α) (D : Set α), V.Countable ∧ Perfect D ∧ C = V ∪ D
have refine_2 : Preperfect D
Tactic: refine ⟨V ∩ C, D, Vct, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
Vct : (V ∩ C).Countable
refine_1 : IsClosed[inst] D
refine_2 : Preperfect D
⊢ ∃ (V : Set α) (D : Set α), V.Countable ∧ Perfect D ∧ C = V ∪ D
have refine_3 : C = V ∩ C ∪ D
Tactic: refine ⟨V ∩ C, D, Vct, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
Vct : (V ∩ C).Countable
⊢ IsClosed[inst] D
have refine_1 : ∀ x ∈ v, IsOpen[inst] x
Tactic: refine hclosed.sdiff (isOpen_biUnion fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
Vct : (V ∩ C).Countable
⊢ Preperfect D
have refine_2 : ∀ x ∈ D, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ D, y ≠ x
Tactic: rw [preperfect_iff_nhds]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
⊢ False
have obtain : ∀ (U : Set α) (hUb : U ∈ b) (xU : x ∈ U) (hU : U ⊆ E), False
Tactic: obtain ⟨U, hUb, xU, hU⟩ : ∃ U ∈ b, x ∈ U ∧ U ⊆ E :=
        (IsTopologicalBasis.mem_nhds_iff bbasis).mp xE
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ (U ∩ C).Countable
have h₁ : U ∩ C ⊆ E ∩ D ∪ V ∩ C
Tactic: apply @Countable.mono _ _ (E ∩ D ∪ V ∩ C)
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
h₁ : U ∩ C ⊆ E ∩ D ∪ V ∩ C
⊢ (U ∩ C).Countable
have hs : (E ∩ D ∪ V ∩ C).Countable
Tactic: apply @Countable.mono _ _ (E ∩ D ∪ V ∩ C)
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
⊢ y ∈ E ∩ D ∪ V ∩ C
have pos : ∀ (h : y ∈ V), y ∈ E ∩ D ∪ V ∩ C
Tactic: by_cases h : y ∈ V
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
pos : ∀ (h : y ∈ V), y ∈ E ∩ D ∪ V ∩ C
⊢ y ∈ E ∩ D ∪ V ∩ C
have neg : ∀ (h : y ∉ V), y ∈ E ∩ D ∪ V ∩ C
Tactic: by_cases h : y ∈ V
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ False
have hU_cnt : (U ∩ C).Countable
Tactic: have hU_cnt : (U ∩ C).Countable := by
        apply @Countable.mono _ _ (E ∩ D ∪ V ∩ C)
        · rintro y ⟨yU, yC⟩
          by_cases h : y ∈ V
          · exact mem_union_right _ (mem_inter h yC)
          · exact mem_union_left _ (mem_inter (hU yU) ⟨yC, h⟩)
        exact Countable.union h Vct
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
hU_cnt : (U ∩ C).Countable
⊢ False
have this : U ∈ v
Tactic: have : U ∈ v := ⟨hUb, hU_cnt⟩
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
hU_cnt : (U ∩ C).Countable
this : U ∈ v
⊢ False
have apply : x ∈ V
Tactic: apply xD.2