awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∀ (a : Set α) (ha : a ∈ v), (a ∩ C).Countable

Tactic:
sep_subset_setOf _ _

Premises used: Set.Mem, setOf, Set.sep_subset_setOf, Set.Subset, Set.Countable
-- 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
⊢ ∀ (a : Set α) (ha : a ∈ v), (a ∩ C).Countable

Tactic:
exact sep_subset_setOf _ _

Premises used: Set.sep_subset_setOf
-- 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 ∩ 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 _ _
-- 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
Vct : (V ∩ C).Countable
⊢ ∃ (V : Set α) (D : Set α), V.Countable ∧ Perfect D ∧ C = V ∪ D

Tactic:
⟨V ∩ C, D, Vct, ⟨?_, ?_⟩, ?_⟩

Premises used: Perfect.mk, Inter.inter, And.intro, Exists.intro
-- 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
Vct : (V ∩ C).Countable
refine_1 : IsClosed[inst] D
refine_2 : Preperfect D
refine_3 : C = V ∩ C ∪ D
⊢ ∃ (V : Set α) (D : Set α), V.Countable ∧ Perfect D ∧ C = V ∪ D

Tactic:
refine ⟨V ∩ C, D, Vct, ⟨?_, ?_⟩, ?_⟩
-- 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
Vct : (V ∩ C).Countable
⊢ IsClosed[inst] D

Tactic:
hclosed.sdiff (isOpen_biUnion fun _ ↦ ?_)

Premises used: IsClosed.sdiff, isOpen_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
Vct : (V ∩ C).Countable
refine_1 : ∀ x ∈ v, IsOpen[inst] x
⊢ IsClosed[inst] D

Tactic:
refine hclosed.sdiff (isOpen_biUnion fun _ ↦ ?_)

Premises used: IsClosed.sdiff, isOpen_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
Vct : (V ∩ C).Countable
x : Set α
⊢ x ∈ v → IsOpen[inst] x

Tactic:
fun ⟨Ub, _⟩ ↦ IsTopologicalBasis.isOpen bbasis Ub

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, _private.0.exists_countable_union_perfect_of_isClosed.match_1, IsOpen
-- 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
Vct : (V ∩ C).Countable
x : Set α
⊢ x ∈ v → IsOpen[inst] x

Tactic:
exact fun ⟨Ub, _⟩ ↦ IsTopologicalBasis.isOpen bbasis Ub
-- 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
Vct : (V ∩ C).Countable
refine_2 : ∀ x ∈ D, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ D, y ≠ x
⊢ Preperfect D

Tactic:
rw [preperfect_iff_nhds]

Premises used: preperfect_iff_nhds
-- 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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
⊢ ∃ U ∈ b, x ∈ U ∧ U ⊆ E

Tactic:
(IsTopologicalBasis.mem_nhds_iff bbasis).mp xE

Premises used: Iff.mp, TopologicalSpace.IsTopologicalBasis.mem_nhds_iff
-- 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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
obtain : ∀ (U : Set α) (hUb : U ∈ b) (xU : x ∈ U) (hU : U ⊆ E), False
⊢ False

Tactic:
obtain ⟨U, hUb, xU, hU⟩ : ∃ U ∈ b, x ∈ U ∧ U ⊆ E :=
        (IsTopologicalBasis.mem_nhds_iff bbasis).mp xE

Premises used: Iff.mp, TopologicalSpace.IsTopologicalBasis.mem_nhds_iff
-- 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
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
hs : (E ∩ D ∪ V ∩ C).Countable
⊢ (U ∩ C).Countable

Tactic:
apply @Countable.mono _ _ (E ∩ D ∪ V ∩ C)

Premises used: Set.Countable.mono
-- 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
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
neg : ∀ (h : y ∉ V), y ∈ E ∩ D ∪ V ∩ C
⊢ y ∈ E ∩ D ∪ V ∩ C

Tactic:
by_cases h : y ∈ V
-- 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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h_1 : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
h : y ∈ V
⊢ y ∈ E ∩ D ∪ V ∩ C

Tactic:
mem_union_right _ (mem_inter h yC)

Premises used: Set.mem_union_right, Set.mem_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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h_1 : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
h : y ∈ V
⊢ y ∈ E ∩ D ∪ V ∩ C

Tactic:
exact mem_union_right _ (mem_inter h yC)

Premises used: Set.mem_union_right, Set.mem_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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h_1 : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
h : y ∉ V
⊢ y ∈ E ∩ D ∪ V ∩ C

Tactic:
mem_union_left _ (mem_inter (hU yU) ⟨yC, h⟩)

Premises used: Set.mem_inter, And.intro, Set.mem_union_left
-- 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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h_1 : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
h : y ∉ V
⊢ y ∈ E ∩ D ∪ V ∩ C

Tactic:
exact mem_union_left _ (mem_inter (hU yU) ⟨yC, h⟩)
-- 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
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
⊢ (E ∩ D ∪ V ∩ C).Countable

Tactic:
Countable.union h Vct

Premises used: Set.Countable.union
-- 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
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
⊢ (E ∩ D ∪ V ∩ C).Countable

Tactic:
exact Countable.union h Vct

Premises used: Set.Countable.union
-- 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
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

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
-- 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
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
⊢ U ∈ v

Tactic:
have : U ∈ v := ⟨hUb, hU_cnt⟩
-- 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
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
apply : x ∈ V
⊢ False

Tactic:
apply xD.2

Premises used: And.right
-- 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
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
⊢ x ∈ V

Tactic:
mem_biUnion this xU

Premises used: Set.Mem, Set.mem_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
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
⊢ x ∈ V

Tactic:
exact mem_biUnion this xU

Premises used: Set.mem_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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
⊢ ¬(E ∩ D).Countable

Tactic:
have : ¬(E ∩ D).Countable := by
      intro h
      obtain ⟨U, hUb, xU, hU⟩ : ∃ U ∈ b, x ∈ U ∧ U ⊆ E :=
        (IsTopologicalBasis.mem_nhds_iff bbasis).mp xE
      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
      have : U ∈ v := ⟨hUb, hU_cnt⟩
      apply xD.2
      exact mem_biUnion this xU
-- 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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
this : ¬(E ∩ D).Countable
refine_2 : ∀ (h : ∀ (y : α) (_ : y ∈ E ∩ D), y = x), False
⊢ ∃ y ∈ E ∩ D, y ≠ x

Tactic:
by_contra! h
-- 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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
this : ¬(E ∩ D).Countable
h : ∀ (y : α) (_ : y ∈ E ∩ D), y = x
⊢ False

Tactic:
absurd (Countable.mono h (Set.countable_singleton _)) this

Premises used: absurd, Set.Countable.mono, Set.countable_singleton
-- 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
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
this : ¬(E ∩ D).Countable
h : ∀ (y : α) (_ : y ∈ E ∩ D), y = x
⊢ False

Tactic:
exact absurd (Countable.mono h (Set.countable_singleton _)) this

Premises used: absurd, Set.Countable.mono, Set.countable_singleton
-- 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
Vct : (V ∩ C).Countable
refine_3 : C = C ∩ V ∪ D
refine_3₁ refine_3₂ : C = C
⊢ C = V ∩ C ∪ D

Tactic:
rw [inter_comm, inter_union_diff]

Premises used: Set.inter_comm, Set.inter_union_diff
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
rcases :
  ∀ (V D : Set α) (Vct : V.Countable) (Dperf : Perfect D) (VD : C = V ∪ D),
    ∃ (D : Set α), Perfect D ∧ D.Nonempty ∧ D ⊆ C
⊢ ∃ (D : Set α), Perfect D ∧ D.Nonempty ∧ D ⊆ C

Tactic:
rcases exists_countable_union_perfect_of_isClosed hclosed with ⟨V, D, Vct, Dperf, VD⟩

Premises used: exists_countable_union_perfect_of_isClosed
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ ∃ (D : Set α), Perfect D ∧ D.Nonempty ∧ D ⊆ C

Tactic:
⟨D, ⟨Dperf, ?_⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
refine : D.Nonempty ∧ D ⊆ C
⊢ ∃ (D : Set α), Perfect D ∧ D.Nonempty ∧ D ⊆ C

Tactic:
refine ⟨D, ⟨Dperf, ?_⟩⟩
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
left : D.Nonempty
right : D ⊆ C
⊢ D.Nonempty ∧ D ⊆ C

Tactic:
constructor
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
left : D ≠ ∅
⊢ D.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
left : ∀ (h : D = ∅), False
⊢ D ≠ ∅

Tactic:
by_contra h
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
h : D = ∅
⊢ C = V

Tactic:
rw [h, union_empty] at VD

Premises used: Set.union_empty
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
h : D = ∅
VD₁ : C = V
⊢ D = ∅

Tactic:
rw [h, union_empty] at VD

Premises used: Set.union_empty
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
left : ∀ (hunc : ¬V.Countable) (D : Set α) (Vct : V.Countable) (Dperf : Perfect D) (VD : C = V) (h : D = ∅), False
⊢ False

Tactic:
rw [VD] at hunc
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
V : Set α
hunc : ¬V.Countable
D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
right : D ⊆ V ∪ D
⊢ D ⊆ C

Tactic:
rw [VD]
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ V ∪ D

Tactic:
subset_union_right

Premises used: Set.subset_union_right
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ V ∪ D

Tactic:
exact subset_union_right

Premises used: Set.subset_union_right
-- Module: Mathlib.Topology.Perfect
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ PerfectSpace X ↔ ∀ (x : X), (𝓝[≠] x).NeBot

Tactic:
simp [perfectSpace_def, Preperfect, AccPt]

Premises used: Preperfect, perfectSpace_def, AccPt
-- Module: Mathlib.Topology.Perfect
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PerfectSpace X
x : X
⊢ (𝓝[≠] x).NeBot

Tactic:
perfectSpace_iff_forall_not_isolated.mp ‹_› x

Premises used: Iff.mp, perfectSpace_iff_forall_not_isolated
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
inst_2 : DecidableEq α
y : β
rw :
  ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) (s \ {x}) x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
rw₁ :
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 (update (β := fun (a : α) ↦ β) f x y x)) ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
rw₂ rw₃ :
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y) ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
⊢ ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) s x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)

Tactic:
rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_self]

Premises used: continuousWithinAt_diff_self, ContinuousWithinAt, Function.update_self
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
inst_2 : DecidableEq α
y : β
rw :
  ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) (s \ {x}) x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
rw₁ :
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 (update (β := fun (a : α) ↦ β) f x y x)) ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
rw₂ rw₃ :
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y) ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
⊢ ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) s x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)

Tactic:
{ rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_self] }

Premises used: continuousWithinAt_diff_self, ContinuousWithinAt, Function.update_self