awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
x : (↑I : Type)
⊢ Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ.cast ⋯ ⋯ : (a : (↑I : Type)) → X) x : X)
have a₁ : Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ : (a : (↑I : Type)) → X) x : X)
Tactic: rw [cast_coe]
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
x : (↑I : Type)
⊢ Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ : (a : (↑I : Type)) → X) x : X)
have this : Membership.mem (γ := Set ℝ) (Icc 0 1) (↑x : ℝ)
Tactic: have : ↑x ∈ (Icc 0 1 : Set ℝ) := x.2
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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 : ℝ)
⊢ Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ : (a : (↑I : Type)) → X) x : X)
have a₁ : Eq (α := X)
  (({ toFun := fun (s : (↑I : Type)) ↦ (γ.extend : (a : ℝ) → X) (min (max (↑s : ℝ) 0) 1), continuous_toFun := sorry,
          source' := sorry, target' := sorry :
          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)
Tactic: rw [truncate, coe_mk_mk, max_eq_left this.1, min_eq_left this.2, extend_extends']
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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)
⊢ Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ : (a : (↑I : Type)) → X) x : X)
have a₂ : Eq (α := X) ((γ.extend : (a : ℝ) → X) (min (max (↑x : ℝ) 0) 1) : 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']
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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)
⊢ Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ : (a : (↑I : Type)) → X) x : X)
have a₃ : Eq (α := X) ((γ.extend : (a : ℝ) → X) (min (↑x : ℝ) 1) : 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']
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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)
⊢ Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ : (a : (↑I : Type)) → X) x : X)
have a₄ : Eq (α := X) ((γ.extend : (a : ℝ) → 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']
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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)
⊢ Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ : (a : (↑I : Type)) → X) x : X)
have a₅ : Eq (α := X) ((γ : (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']
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.reparam id ⋯ ⋯ ⋯ = γ
have a : ∀ (x_1 : (↑I : Type)),
  Eq (α := X) ((γ.reparam id sorry sorry sorry : (a : (↑I : Type)) → X) x_1 : X) ((γ : (a : (↑I : Type)) → X) x_1 : X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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 (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.reparam f hfcont hf₀ hf₁) : (a : (↑I : Type)) → X))
    (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
have change : Eq (α := Set X) (range ((⇑γ : (a : (↑I : Type)) → X) ∘ f)) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
Tactic: change range (γ ∘ f) = range γ
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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
have rw : Surjective f
Tactic: rw [range_eq_univ]
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
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)
⊢ ∃ (a : (↑I : Type)), f a = t
have h₁ : Continuous (IccExtend sorry f)
Tactic: have h₁ : Continuous (Set.IccExtend (zero_le_one' ℝ) f) := by fun_prop
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
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)
⊢ ∃ (a : (↑I : Type)), f a = t
have this : Icc (IccExtend sorry f 0) (IccExtend sorry f 1) ⊆ IccExtend sorry f '' Icc 0 1
Tactic: have := intermediate_value_Icc (zero_le_one' ℝ) h₁.continuousOn
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
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
⊢ ∃ (a : (↑I : Type)), f a = t
have this₁ : Icc 0 1 ⊆ IccExtend sorry f '' Icc 0 1
Tactic: rw [IccExtend_left, IccExtend_right, Icc.mk_zero, Icc.mk_one, hf₀, hf₁] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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
⊢ ∃ (a : (↑I : Type)), f a = t
have rcases : ∀ (w : ℝ) (hw₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) w) (hw₂ : IccExtend sorry f w = t), ∃ (a : (↑I : Type)), f a = t
Tactic: rcases this t.2 with ⟨w, hw₁, hw₂⟩
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
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
⊢ ∃ (a : (↑I : Type)), f a = t
have hw₃ : f (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) w hw₁) = t
Tactic: rw [IccExtend_of_mem _ _ hw₁] at hw₂
Cleared hypotheses: hw₂
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
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 (α := Set X) (range ((⇑γ : (a : (↑I : Type)) → X) ∘ f)) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
have this : 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₂⟩
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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
⊢ Eq (α := Set X) (range ((⇑γ : (a : (↑I : Type)) → X) ∘ f)) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
have rw : Eq (α := Set X) ((⇑γ : (a : (↑I : Type)) → X) '' range f) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
Tactic: rw [range_comp, this, image_univ]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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))
⊢ Eq (α := Set X) (range ((⇑γ : (a : (↑I : Type)) → X) ∘ f)) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
have rw₁ : Eq (α := Set X) (image (α := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) univ)
  (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
Tactic: rw [range_comp, this, image_univ]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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))
⊢ Eq (α := Set X) (range ((⇑γ : (a : (↑I : Type)) → X) ∘ f)) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
have rw₂ : Eq (α := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
  (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
Tactic: rw [range_comp, this, image_univ]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
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
⊢ Eq (α := Path x x) (reparam (refl x) f hfcont hf₀ hf₁) (refl x)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ 𝓝[≠] x ≤ 𝓟 U
have rw : U ∈ 𝓝[≠] x
Tactic: rw [le_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ AccPt x (𝓟 (U ∩ C))
have this : 𝓝[≠] x ≤ 𝓟 U
Tactic: have : 𝓝[≠] x ≤ 𝓟 U := by
    rw [le_principal_iff]
    exact mem_nhdsWithin_of_mem_nhds hU
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ AccPt x (𝓟 (U ∩ C))
have rw : (𝓝[≠] x ⊓ 𝓟 C).NeBot
Tactic: rw [AccPt, ← inf_principal, ← inf_assoc, inf_of_le_left this]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen[inst] U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ AccPt x (𝓟 (U ∩ C))
have apply : U ∈ 𝓝 x
Tactic: apply (hC _ xC).nhds_inter
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
⊢ Perfect (closure[inst] C)
have closed : IsClosed[inst] (closure[inst] C)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
closed : IsClosed[inst] (closure[inst] C)
⊢ Perfect (closure[inst] C)
have acc : Preperfect (closure[inst] C)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
⊢ AccPt x (𝓟 (closure[inst] C))
have pos : ∀ (h : x ∈ C), AccPt x (𝓟 (closure[inst] C))
Tactic: by_cases h : x ∈ C
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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))
⊢ AccPt x (𝓟 (closure[inst] C))
have neg : ∀ (h : x ∉ C), AccPt x (𝓟 (closure[inst] C))
Tactic: by_cases h : x ∈ C
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∈ C
⊢ AccPt x (𝓟 (closure[inst] C))
have apply : AccPt x (𝓟 C)
Tactic: apply AccPt.mono _ (principal_mono.mpr subset_closure)
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∉ C
⊢ AccPt x (𝓟 (closure[inst] C))
have apply : AccPt x (𝓟 C)
Tactic: apply AccPt.mono _ (principal_mono.mpr subset_closure)
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∉ C
⊢ AccPt x (𝓟 C)
have this : {x}ᶜ ∩ C = C
Tactic: have : {x}ᶜ ∩ C = C := by simp [h]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ AccPt x (𝓟 C)
have rw : (𝓝 x ⊓ 𝓟 C).NeBot
Tactic: rw [AccPt, nhdsWithin, inf_assoc, inf_principal, this]
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot
have hx₁ : Membership.mem (γ := Set α) {a : α | ClusterPt a (𝓟 C)} x
Tactic: rw [closure_eq_cluster_pts] at hx
Cleared hypotheses: hx, h, this
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
⊢ Preperfect C ↔ Perfect (closure[inst] C)
have mp : Preperfect C → Perfect (closure[inst] C)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
mp : Preperfect C → Perfect (closure[inst] C)
⊢ Preperfect C ↔ Perfect (closure[inst] C)
have mpr : Perfect (closure[inst] C) → Preperfect C
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T1Space α
h : Perfect (closure[inst] C)
x : α
xC : x ∈ C
⊢ AccPt x (𝓟 C)
have H : AccPt x (𝓟 (closure[inst] C))
Tactic: have H : AccPt x (𝓟 (closure C)) := h.acc _ (subset_closure xC)
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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))
⊢ AccPt x (𝓟 C)
have mpr : ∀ (H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst] C), ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C
Tactic: rw [accPt_iff_frequently] at *
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
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 : α) in 𝓝 x, y ≠ x ∧ y ∈ C
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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
⊢ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C
have mpr : ∃ᶠ (x' : α) in 𝓝 x, ∃ᶠ (x'' : α) in 𝓝 x', x'' ≠ x ∧ x'' ∈ C
Tactic: rw [← frequently_frequently_nhds]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst] U
⊢ Perfect (closure[inst] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty
have left : Perfect (closure[inst] (U ∩ C))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
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))
⊢ Perfect (closure[inst] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty
have right : (closure[inst] (U ∩ C)).Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst] U
⊢ Perfect (closure[inst] (U ∩ C))
have left : Preperfect (U ∩ C)
Tactic: apply Preperfect.perfect_closure
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst] U
⊢ (closure[inst] (U ∩ C)).Nonempty
have right : (U ∩ C).Nonempty
Tactic: apply Nonempty.closure
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
hnonempty : C.Nonempty
⊢ ∃ (C₀ : Set α) (C₁ : Set α),
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
have obtain : ∀ (y : α) (yC : y ∈ 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
Cleared hypotheses: hnonempty
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
⊢ ∃ x ∈ C, x ≠ y
have this : AccPt y (𝓟 C)
Tactic: have := hC.acc _ yC
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : AccPt y (𝓟 C)
⊢ ∃ x ∈ C, x ≠ y
have this₁ : ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y
Tactic: rw [accPt_iff_nhds] at this
Cleared hypotheses: this
-- 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
this : ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y
⊢ ∃ x ∈ C, x ≠ y
have rcases : ∀ (x : α) (xC : x ∈ univ ∩ C) (hxy : x ≠ y), ∃ x ∈ C, x ≠ y
Tactic: rcases this univ univ_mem with ⟨x, xC, hxy⟩
-- 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
⊢ ∃ (C₀ : Set α) (C₁ : Set α),
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
have 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₁
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⟩
-- 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
⊢ ∃ (C₀ : Set α) (C₁ : Set α),
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
have 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₁
Tactic: obtain ⟨U, xU, Uop, V, yV, Vop, hUV⟩ := exists_open_nhds_disjoint_closure hxy
-- 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)
⊢ ∃ (C₀ : Set α) (C₁ : Set α),
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
have 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))
Tactic: use closure (U ∩ C), closure (V ∩ C)
-- 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) ∧
    (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] (U ∩ C)) ∧ (closure[inst] (U ∩ C)).Nonempty ∧ closure[inst] (U ∩ C) ⊆ C
Tactic: constructor