awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
x : (↑I : Type)
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) (↑x : ℝ)

Tactic:
have : ↑x ∈ (Icc 0 1 : Set ℝ) := x.2
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
x : (↑I : Type)
this : Membership.mem (γ := Set ℝ) (Icc 0 1) (↑x : ℝ)
a₁ :
  Eq (α := X)
    (({ toFun := fun (s : (↑I : Type)) ↦ (γ.extend : (a : ℝ) → X) (min (max (↑s : ℝ) 0) 1), continuous_toFun := ⋯,
            source' := ⋯, target' := ⋯ :
            Path (X := X) ((γ.extend : (a : ℝ) → X) (min 0 1) : X) ((γ.extend : (a : ℝ) → X) 1 : X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((γ : (a : (↑I : Type)) → X) x : X)
a₂ : Eq (α := X) ((γ.extend : (a : ℝ) → X) (min (max (↑x : ℝ) 0) 1) : X) ((γ : (a : (↑I : Type)) → X) x : X)
a₃ : Eq (α := X) ((γ.extend : (a : ℝ) → X) (min (↑x : ℝ) 1) : X) ((γ : (a : (↑I : Type)) → X) x : X)
a₄ : Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑x : ℝ) : X) ((γ : (a : (↑I : Type)) → X) x : X)
a₅ a₆ : Eq (α := X) ((γ : (a : (↑I : Type)) → X) x : X) ((γ : (a : (↑I : Type)) → X) x : X)
⊢ Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ : (a : (↑I : Type)) → X) x : X)

Tactic:
rw [truncate, coe_mk_mk, max_eq_left this.1, min_eq_left this.2, extend_extends']

Premises used: Path.truncate, max_eq_left, min_eq_left, And.right, And.left, Path.coe_mk_mk, Path.extend_extends'
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ_1 γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ Continuous[_, inst] ((⇑γ : (a : (↑I : Type)) → X) ∘ f)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ_1 γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ ((⇑γ : (a : (↑I : Type)) → X) ∘ f) 0 = x

Tactic:
simp [hf₀]
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ_1 γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ ((⇑γ : (a : (↑I : Type)) → X) ∘ f) 1 = y

Tactic:
simp [hf₁]
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ Eq (α := (a : (↑I : Type)) → X) (⇑(γ.reparam f hfcont hf₀ hf₁) : (a : (↑I : Type)) → X)
    ((⇑γ : (a : (↑I : Type)) → X) ∘ f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
a :
  ∀ (x_1 : (↑I : Type)),
    Eq (α := X) ((γ.reparam id ⋯ ⋯ ⋯ : (a : (↑I : Type)) → X) x_1 : X) ((γ : (a : (↑I : Type)) → X) x_1 : X)
⊢ γ.reparam id ⋯ ⋯ ⋯ = γ

Tactic:
ext
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
x_1 : (↑I : Type)
⊢ Eq (α := X) ((γ.reparam id ⋯ ⋯ ⋯ : (a : (↑I : Type)) → X) x_1 : X) ((γ : (a : (↑I : Type)) → X) x_1 : X)

Tactic:
rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
change :
  Eq (α := Set X) (range ((⇑γ : (a : (↑I : Type)) → X) ∘ f)) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.reparam f hfcont hf₀ hf₁) : (a : (↑I : Type)) → X))
    (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))

Tactic:
change range (γ ∘ f) = range γ

Premises used: Function.comp, Set.range, DFunLike.coe
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
rw : Surjective f
⊢ range f = univ

Tactic:
rw [range_eq_univ]

Premises used: Set.range_eq_univ
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : (↑I : Type)
⊢ Continuous (IccExtend ⋯ f)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : (↑I : Type)
⊢ Continuous (IccExtend ⋯ f)

Tactic:
have h₁ : Continuous (Set.IccExtend (zero_le_one' ℝ) f) := by fun_prop
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : (↑I : Type)
h₁ : Continuous (IccExtend ⋯ f)
⊢ Icc (IccExtend ⋯ f 0) (IccExtend ⋯ f 1) ⊆ IccExtend ⋯ f '' Icc 0 1

Tactic:
have := intermediate_value_Icc (zero_le_one' ℝ) h₁.continuousOn
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : (↑I : Type)
h₁ : Continuous (IccExtend ⋯ f)
this : Icc (IccExtend ⋯ f 0) (IccExtend ⋯ f 1) ⊆ IccExtend ⋯ f '' Icc 0 1
⊢ Icc 0 1 ⊆ IccExtend ⋯ f '' Icc 0 1

Tactic:
rw [IccExtend_left, IccExtend_right, Icc.mk_zero, Icc.mk_one, hf₀, hf₁] at this

Premises used: Set.Icc.mk_zero, Set.IccExtend_right, Set.IccExtend_left, Set.Icc.mk_one
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : (↑I : Type)
h₁ : Continuous (IccExtend ⋯ f)
this : Icc 0 1 ⊆ IccExtend ⋯ f '' Icc 0 1
rcases :
  ∀ (w : ℝ) (hw₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) w) (hw₂ : IccExtend ⋯ f w = t), ∃ (a : (↑I : Type)), f a = t
⊢ ∃ (a : (↑I : Type)), f a = t

Tactic:
rcases this t.2 with ⟨w, hw₁, hw₂⟩

Premises used: Subtype.property
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : (↑I : Type)
h₁ : Continuous (IccExtend ⋯ f)
this : Icc 0 1 ⊆ IccExtend ⋯ f '' Icc 0 1
w : ℝ
hw₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) w
hw₂ : IccExtend ⋯ f w = t
⊢ f (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) w hw₁) = t

Tactic:
rw [IccExtend_of_mem _ _ hw₁] at hw₂

Premises used: Set.IccExtend_of_mem
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : (↑I : Type)
h₁ : Continuous (IccExtend ⋯ f)
this : Icc 0 1 ⊆ IccExtend ⋯ f '' Icc 0 1
w : ℝ
hw₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) w
hw₂ : f (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) w hw₁) = t
⊢ ∃ (a : (↑I : Type)), f a = t

Tactic:
⟨_, hw₂⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : (↑I : Type)
h₁ : Continuous (IccExtend ⋯ f)
this : Icc 0 1 ⊆ IccExtend ⋯ f '' Icc 0 1
w : ℝ
hw₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) w
hw₂ : f (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) w hw₁) = t
⊢ ∃ (a : (↑I : Type)), f a = t

Tactic:
exact ⟨_, hw₂⟩
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ range f = univ

Tactic:
have : range f = univ := by
    rw [range_eq_univ]
    intro t
    have h₁ : Continuous (Set.IccExtend (zero_le_one' ℝ) f) := by fun_prop
    have := intermediate_value_Icc (zero_le_one' ℝ) h₁.continuousOn
    · rw [IccExtend_left, IccExtend_right, Icc.mk_zero, Icc.mk_one, hf₀, hf₁] at this
      rcases this t.2 with ⟨w, hw₁, hw₂⟩
      rw [IccExtend_of_mem _ _ hw₁] at hw₂
      exact ⟨_, hw₂⟩
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
this : range f = univ
rw : Eq (α := Set X) ((⇑γ : (a : (↑I : Type)) → X) '' range f) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
rw₁ :
  Eq (α := Set X) (image (α := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) univ)
    (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
rw₂ rw₃ :
  Eq (α := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
    (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
⊢ Eq (α := Set X) (range ((⇑γ : (a : (↑I : Type)) → X) ∘ f)) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))

Tactic:
rw [range_comp, this, image_univ]

Premises used: Set.range_comp, Set.image_univ
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
a :
  ∀ (x_1 : (↑I : Type)),
    Eq (α := X) ((reparam (refl x) f hfcont hf₀ hf₁ : (a : (↑I : Type)) → X) x_1 : X)
      ((refl x : (a : (↑I : Type)) → X) x_1 : X)
⊢ Eq (α := Path x x) (reparam (refl x) f hfcont hf₀ hf₁) (refl x)

Tactic:
ext
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
f : (↑I : Type) → (↑I : Type)
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x_1 : (↑I : Type)
⊢ Eq (α := X) ((reparam (refl x) f hfcont hf₀ hf₁ : (a : (↑I : Type)) → X) x_1 : X)
    ((refl x : (a : (↑I : Type)) → X) x_1 : X)

Tactic:
simp
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
rw : U ∈ 𝓝[≠] x
⊢ 𝓝[≠] x ≤ 𝓟 U

Tactic:
rw [le_principal_iff]

Premises used: Filter.le_principal_iff
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ U ∈ 𝓝[≠] x

Tactic:
mem_nhdsWithin_of_mem_nhds hU

Premises used: mem_nhdsWithin_of_mem_nhds
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ U ∈ 𝓝[≠] x

Tactic:
exact mem_nhdsWithin_of_mem_nhds hU

Premises used: mem_nhdsWithin_of_mem_nhds
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ 𝓝[≠] x ≤ 𝓟 U

Tactic:
have : 𝓝[≠] x ≤ 𝓟 U := by
    rw [le_principal_iff]
    exact mem_nhdsWithin_of_mem_nhds hU
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
rw : (𝓝[≠] x ⊓ 𝓟 C).NeBot
⊢ AccPt x (𝓟 (U ∩ C))

Tactic:
rw [AccPt, ← inf_principal, ← inf_assoc, inf_of_le_left this]

Premises used: Filter.inf_principal, inf_of_le_left, AccPt, inf_assoc
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ (𝓝[≠] x ⊓ 𝓟 C).NeBot

Tactic:
h_acc

Premises used: AccPt
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ (𝓝[≠] x ⊓ 𝓟 C).NeBot

Tactic:
exact h_acc
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
⊢ Preperfect C ↔ ∀ x ∈ C, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x

Tactic:
simp only [Preperfect, accPt_iff_nhds]

Premises used: Preperfect, accPt_iff_nhds
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PerfectSpace α
⊢ Perfect.{u_1} (α := α) univ

Tactic:
⟨isClosed_univ, PerfectSpace.univ_preperfect⟩

Premises used: isClosed_univ, Perfect.mk, PerfectSpace.univ_preperfect
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen[inst] U
x : α
xU : x ∈ U
xC : x ∈ C
apply : U ∈ 𝓝 x
⊢ AccPt x (𝓟 (U ∩ C))

Tactic:
apply (hC _ xC).nhds_inter

Premises used: AccPt.nhds_inter
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen[inst] U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ U ∈ 𝓝 x

Tactic:
hU.mem_nhds xU

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen[inst] U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ U ∈ 𝓝 x

Tactic:
exact hU.mem_nhds xU

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
closed : IsClosed[inst] (closure[inst] C)
acc : Preperfect (closure[inst] C)
⊢ Perfect (closure[inst] C)

Tactic:
constructor
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
⊢ IsClosed[inst] (closure[inst] C)

Tactic:
isClosed_closure

Premises used: isClosed_closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
⊢ IsClosed[inst] (closure[inst] C)

Tactic:
exact isClosed_closure

Premises used: isClosed_closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
pos : ∀ (h : x ∈ C), AccPt x (𝓟 (closure[inst] C))
neg : ∀ (h : x ∉ C), AccPt x (𝓟 (closure[inst] C))
⊢ AccPt x (𝓟 (closure[inst] C))

Tactic:
by_cases h : x ∈ C
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∈ C
apply : AccPt x (𝓟 C)
⊢ AccPt x (𝓟 (closure[inst] C))

Tactic:
apply AccPt.mono _ (principal_mono.mpr subset_closure)

Premises used: Iff.mpr, AccPt.mono, Filter.principal_mono, subset_closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∉ C
apply : AccPt x (𝓟 C)
⊢ AccPt x (𝓟 (closure[inst] C))

Tactic:
apply AccPt.mono _ (principal_mono.mpr subset_closure)

Premises used: Iff.mpr, AccPt.mono, Filter.principal_mono, subset_closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∈ C
⊢ AccPt x (𝓟 C)

Tactic:
hC _ h
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∈ C
⊢ AccPt x (𝓟 C)

Tactic:
exact hC _ h
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∉ C
⊢ {x}ᶜ ∩ C = C

Tactic:
simp [h]
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∉ C
⊢ {x}ᶜ ∩ C = C

Tactic:
have : {x}ᶜ ∩ C = C := by simp [h]
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
rw : (𝓝 x ⊓ 𝓟 C).NeBot
⊢ AccPt x (𝓟 C)

Tactic:
rw [AccPt, nhdsWithin, inf_assoc, inf_principal, this]

Premises used: Filter.inf_principal, nhdsWithin, AccPt, inf_assoc
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ Membership.mem (γ := Set α) {a : α | ClusterPt a (𝓟 C)} x

Tactic:
rw [closure_eq_cluster_pts] at hx

Premises used: closure_eq_cluster_pts
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
hx₁ : Membership.mem (γ := Set α) {a : α | ClusterPt a (𝓟 C)} x
⊢ x ∉ C

Tactic:
rw [closure_eq_cluster_pts] at hx

Premises used: closure_eq_cluster_pts
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
hx₁ : Membership.mem (γ := Set α) {a : α | ClusterPt a (𝓟 C)} x
h₁ : x ∉ C
⊢ {x}ᶜ ∩ C = C

Tactic:
rw [closure_eq_cluster_pts] at hx

Premises used: closure_eq_cluster_pts
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : Membership.mem (γ := Set α) {a : α | ClusterPt a (𝓟 C)} x
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot

Tactic:
hx

Premises used: Set.Mem, setOf, ClusterPt
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : Membership.mem (γ := Set α) {a : α | ClusterPt a (𝓟 C)} x
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot

Tactic:
exact hx
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PerfectSpace α
U : Set α
hU : IsOpen[inst] U
⊢ Preperfect U

Tactic:
simpa using PerfectSpace.univ_preperfect.open_inter hU

Premises used: PerfectSpace.univ_preperfect, Preperfect.open_inter
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PerfectSpace α
U : Set α
hU : IsOpen[inst] U
⊢ Perfect (closure[inst] U)

Tactic:
hU.preperfect.perfect_closure

Premises used: Preperfect.perfect_closure, IsOpen.preperfect
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
mp : Preperfect C → Perfect (closure[inst] C)
mpr : Perfect (closure[inst] C) → Preperfect C
⊢ Preperfect C ↔ Perfect (closure[inst] C)

Tactic:
constructor
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Preperfect C
⊢ Perfect (closure[inst] C)

Tactic:
h.perfect_closure

Premises used: Preperfect.perfect_closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Preperfect C
⊢ Perfect (closure[inst] C)

Tactic:
exact h.perfect_closure

Premises used: Preperfect.perfect_closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Perfect (closure[inst] C)
x : α
xC : x ∈ C
⊢ AccPt x (𝓟 (closure[inst] C))

Tactic:
have H : AccPt x (𝓟 (closure C)) := h.acc _ (subset_closure xC)
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Perfect (closure[inst] C)
x : α
xC : x ∈ C
H : AccPt x (𝓟 (closure[inst] C))
mpr : ∀ (H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst] C), ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C
⊢ AccPt x (𝓟 C)

Tactic:
rw [accPt_iff_frequently] at *

Premises used: accPt_iff_frequently
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Perfect (closure[inst] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst] C
y : α
hyx : y ≠ x
yC simp : y ∈ closure[inst] C
⊢ ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C

Tactic:
simp only [← mem_compl_singleton_iff, and_comm, ← frequently_nhdsWithin_iff,
      hyx.nhdsWithin_compl_singleton, ← mem_closure_iff_frequently]

Premises used: mem_closure_iff_frequently, Ne.nhdsWithin_compl_singleton, and_comm, Set.mem_compl_singleton_iff, frequently_nhdsWithin_iff
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Perfect (closure[inst] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst] C
y : α
hyx : y ≠ x
yC : y ∈ closure[inst] C
⊢ y ∈ closure[inst] C

Tactic:
yC
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Perfect (closure[inst] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst] C
y : α
hyx : y ≠ x
yC : y ∈ closure[inst] C
⊢ y ∈ closure[inst] C

Tactic:
exact yC
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Perfect (closure[inst] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst] C
⊢ ∀ (y : α), y ≠ x ∧ y ∈ closure[inst] C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C

Tactic:
have : ∀ y, y ≠ x ∧ y ∈ closure C → ∃ᶠ z in 𝓝 y, z ≠ x ∧ z ∈ C := by
    rintro y ⟨hyx, yC⟩
    simp only [← mem_compl_singleton_iff, and_comm, ← frequently_nhdsWithin_iff,
      hyx.nhdsWithin_compl_singleton, ← mem_closure_iff_frequently]
    exact yC
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Perfect (closure[inst] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst] C
this : ∀ (y : α), y ≠ x ∧ y ∈ closure[inst] C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C
mpr : ∃ᶠ (x' : α) in 𝓝 x, ∃ᶠ (x'' : α) in 𝓝 x', x'' ≠ x ∧ x'' ∈ C
⊢ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C

Tactic:
rw [← frequently_frequently_nhds]

Premises used: frequently_frequently_nhds
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Perfect (closure[inst] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst] C
this : ∀ (y : α), y ≠ x ∧ y ∈ closure[inst] C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C
⊢ ∃ᶠ (x' : α) in 𝓝 x, ∃ᶠ (x'' : α) in 𝓝 x', x'' ≠ x ∧ x'' ∈ C

Tactic:
H.mono this

Premises used: Filter.Frequently.mono
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Perfect (closure[inst] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst] C
this : ∀ (y : α), y ≠ x ∧ y ∈ closure[inst] C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C
⊢ ∃ᶠ (x' : α) in 𝓝 x, ∃ᶠ (x'' : α) in 𝓝 x', x'' ≠ x ∧ x'' ∈ C

Tactic:
exact H.mono this

Premises used: Filter.Frequently.mono
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst] U
left : Perfect (closure[inst] (U ∩ C))
right : (closure[inst] (U ∩ C)).Nonempty
⊢ Perfect (closure[inst] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty

Tactic:
constructor
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst] U
left : Preperfect (U ∩ C)
⊢ Perfect (closure[inst] (U ∩ C))

Tactic:
apply Preperfect.perfect_closure

Premises used: Preperfect.perfect_closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst] U
⊢ Preperfect (U ∩ C)

Tactic:
hC.acc.open_inter Uop

Premises used: Perfect.acc, Preperfect.open_inter
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst] U
⊢ Preperfect (U ∩ C)

Tactic:
exact hC.acc.open_inter Uop

Premises used: Perfect.acc, Preperfect.open_inter
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst] U
right : (U ∩ C).Nonempty
⊢ (closure[inst] (U ∩ C)).Nonempty

Tactic:
apply Nonempty.closure

Premises used: Set.Nonempty.closure
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst] U
⊢ (U ∩ C).Nonempty

Tactic:
⟨x, ⟨xU, xC⟩⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst] U
⊢ (U ∩ C).Nonempty

Tactic:
exact ⟨x, ⟨xU, xC⟩⟩
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
hnonempty : C.Nonempty
obtain :
  ∀ (y : α) (yC : y ∈ C),
    ∃ (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 ⟨y, yC⟩ := hnonempty
-- Module: Mathlib.Topology.Perfect
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
⊢ AccPt y (𝓟 C)

Tactic:
have := hC.acc _ yC