awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
y : OnePoint X
infty :
  Inseparable.{u_1} (X := OnePoint X) ∞ ∞ ↔
    Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∧ Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∨
      ∃ (x' : X), ∞ = (↑x' : OnePoint X) ∧ ∃ (y' : X), ∞ = (↑y' : OnePoint X) ∧ Inseparable x' y'
⊢ Inseparable ∞ y ↔
    Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∧ y = ∞ ∨
      ∃ (x' : X), ∞ = (↑x' : OnePoint X) ∧ ∃ (y' : X), y = (↑y' : OnePoint X) ∧ Inseparable x' y'
have infty₁ : ∀ (x : X),
  Inseparable ∞ (↑x : OnePoint X) ↔
    Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∧ (↑x : OnePoint X) = ∞ ∨
      ∃ (x' : X), ∞ = (↑x' : OnePoint X) ∧ ∃ (y' : X), (↑x : OnePoint X) = (↑y' : OnePoint X) ∧ Inseparable x' y'
Tactic: induction y using OnePoint.rec
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
y : OnePoint X
x : X
⊢ Inseparable (↑x : OnePoint X) y ↔
    (↑x : OnePoint X) = ∞ ∧ y = ∞ ∨
      ∃ (x' : X), (↑x : OnePoint X) = (↑x' : OnePoint X) ∧ ∃ (y' : X), y = (↑y' : OnePoint X) ∧ Inseparable x' y'
have coe : Inseparable (↑x : OnePoint X) ∞ ↔
  (↑x : OnePoint X) = ∞ ∧ Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∨
    ∃ (x' : X), (↑x : OnePoint X) = (↑x' : OnePoint X) ∧ ∃ (y' : X), ∞ = (↑y' : OnePoint X) ∧ Inseparable x' y'
Tactic: induction y using OnePoint.rec
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
y : OnePoint X
x : X
coe :
  Inseparable (↑x : OnePoint X) ∞ ↔
    (↑x : OnePoint X) = ∞ ∧ Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∨
      ∃ (x' : X), (↑x : OnePoint X) = (↑x' : OnePoint X) ∧ ∃ (y' : X), ∞ = (↑y' : OnePoint X) ∧ Inseparable x' y'
⊢ Inseparable (↑x : OnePoint X) y ↔
    (↑x : OnePoint X) = ∞ ∧ y = ∞ ∨
      ∃ (x' : X), (↑x : OnePoint X) = (↑x' : OnePoint X) ∧ ∃ (y' : X), y = (↑y' : OnePoint X) ∧ Inseparable x' y'
have coe₁ : ∀ (x_1 : X),
  Inseparable (↑x : OnePoint X) (↑x_1 : OnePoint X) ↔
    (↑x : OnePoint X) = ∞ ∧ (↑x_1 : OnePoint X) = ∞ ∨
      ∃ (x' : X),
        (↑x : OnePoint X) = (↑x' : OnePoint X) ∧
          ∃ (y' : X), (↑x_1 : OnePoint X) = (↑y' : OnePoint X) ∧ Inseparable x' y'
Tactic: induction y using OnePoint.rec
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (OnePoint.map f) ↔
    Continuous[inst, inst_1] f ∧ Tendsto f (coclosedCompact X) (coclosedCompact Y)
have simp_rw : (Tendsto.{u_1, u_2} (β := OnePoint Y) (fun (x : X) ↦ (↑(f x) : OnePoint Y)) (comap some (𝓝 ∞)) (𝓝 ∞) ∧
    Continuous[inst, instTopologicalSpace] fun (x : X) ↦ (↑(f x) : OnePoint Y)) ↔
  Continuous[inst, instTopologicalSpace] (some ∘ f) ∧ Tendsto (some ∘ f) (comap some (𝓝 ∞)) (𝓝 ∞)
Tactic: simp_rw [continuous_iff, map_some, ← comap_coe_nhds_infty, tendsto_comap_iff, map_infty,
    isOpenEmbedding_coe.isInducing.continuous_iff (Y := Y)]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
⊢ Tendsto some (cocompact X) (𝓝 ∞)
have rw : Tendsto some (cocompact X) (map some (coclosedCompact X) ⊔ pure ∞)
Tactic: rw [nhds_infty_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
⊢ IsCompact.{u_1} (X := OnePoint X) univ
have this : Tendsto some (cocompact X) (𝓝 ∞)
Tactic: have : Tendsto ((↑) : X → OnePoint X) (cocompact X) (𝓝 ∞) := by
      rw [nhds_infty_eq]
      exact (tendsto_map.mono_left cocompact_le_coclosedCompact).mono_right le_sup_left
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact.{u_1} (X := OnePoint X) univ
have rw : IsCompact (X := OnePoint X) (insert none (range Option.some))
Tactic: rw [← insert_none_range_some X]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T0Space X
⊢ T0Space.{u_1} (OnePoint X)
have refine : ∀ (x y : OnePoint X) (hxy : Inseparable x y), x = y
Tactic: refine ⟨fun x y hxy => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T0Space X
x y : OnePoint X
hxy : Inseparable x y
⊢ x = y
have inl : ∀ (hxy : Inseparable.{u_1} (X := OnePoint X) ∞ ∞), Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞
Tactic: rcases inseparable_iff.1 hxy with (⟨rfl, rfl⟩ | ⟨x, rfl, y, rfl, h⟩)
Cleared hypotheses: x, y, hxy
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T0Space X
x y : OnePoint X
hxy : Inseparable x y
inl : ∀ (hxy : Inseparable.{u_1} (X := OnePoint X) ∞ ∞), Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞
⊢ x = y
have inr : ∀ (x y : X) (h : Inseparable x y) (hxy : Inseparable (↑x : OnePoint X) (↑y : OnePoint X)),
  (↑x : OnePoint X) = (↑y : OnePoint X)
Tactic: rcases inseparable_iff.1 hxy with (⟨rfl, rfl⟩ | ⟨x, rfl, y, rfl, h⟩)
Cleared hypotheses: x, y, hxy
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T1Space X
z : OnePoint X
⊢ IsClosed[instTopologicalSpace] {z}
have infty : IsClosed[instTopologicalSpace] {∞}
Tactic: induction z using OnePoint.rec
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T1Space X
z : OnePoint X
infty : IsClosed[instTopologicalSpace] {∞}
⊢ IsClosed[instTopologicalSpace] {z}
have coe : ∀ (x : X), IsClosed[instTopologicalSpace] {(↑x : OnePoint X)}
Tactic: induction z using OnePoint.rec
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T1Space X
x : X
⊢ IsClosed[instTopologicalSpace] {(↑x : OnePoint X)}
have coe : IsClosed[inst] {x} ∧ IsCompact (X := X) {x}
Tactic: rw [← image_singleton, isClosed_image_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
⊢ NormalSpace.{u_1} (OnePoint X)
have suffices : R1Space.{u_1} (OnePoint X)
Tactic: suffices R1Space (OnePoint X) by infer_instance
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
z : X
⊢ Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
have rw : Disjoint (𝓝 z) (cocompact X) ∧ range some ∈ map some (𝓝 z)
Tactic: rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact,
      disjoint_map coe_injective, ← principal_singleton, disjoint_principal_right, compl_infty]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
⊢ R1Space.{u_1} (OnePoint X)
have key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
Tactic: have key : ∀ z : X, Disjoint (𝓝 (some z)) (𝓝 ∞) := fun z ↦ by
    rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact,
      disjoint_map coe_injective, ← principal_singleton, disjoint_principal_right, compl_infty]
    exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
⊢ R1Space.{u_1} (OnePoint X)
have refine : ∀ (x y : OnePoint X), x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)
Tactic: refine ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
x y : OnePoint X
⊢ x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)
have infty : ∞ ⤳ y ∨ Disjoint (𝓝 ∞) (𝓝 y)
Tactic: induction x using OnePoint.rec
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
x y : OnePoint X
infty : ∞ ⤳ y ∨ Disjoint (𝓝 ∞) (𝓝 y)
⊢ x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)
have coe : ∀ (x : X), (↑x : OnePoint X) ⤳ y ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 y)
Tactic: induction x using OnePoint.rec
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
y : OnePoint X
⊢ ∞ ⤳ y ∨ Disjoint (𝓝 ∞) (𝓝 y)
have infty : Specializes.{u_1} (X := OnePoint X) ∞ ∞ ∨ Disjoint.{u_1} (α := Filter (OnePoint X)) (𝓝 ∞) (𝓝 ∞)
Tactic: induction y using OnePoint.rec
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
y : OnePoint X
infty : Specializes.{u_1} (X := OnePoint X) ∞ ∞ ∨ Disjoint.{u_1} (α := Filter (OnePoint X)) (𝓝 ∞) (𝓝 ∞)
⊢ ∞ ⤳ y ∨ Disjoint (𝓝 ∞) (𝓝 y)
have infty₁ : ∀ (x : X), ∞ ⤳ (↑x : OnePoint X) ∨ Disjoint (𝓝 ∞) (𝓝 (↑x : OnePoint X))
Tactic: induction y using OnePoint.rec
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
y : OnePoint X
x : X
⊢ (↑x : OnePoint X) ⤳ y ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 y)
have coe : (↑x : OnePoint X) ⤳ ∞ ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 ∞)
Tactic: induction y using OnePoint.rec
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
y : OnePoint X
x : X
coe : (↑x : OnePoint X) ⤳ ∞ ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 ∞)
⊢ (↑x : OnePoint X) ⤳ y ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 y)
have coe₁ : ∀ (x_1 : X), (↑x : OnePoint X) ⤳ (↑x_1 : OnePoint X) ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 (↑x_1 : OnePoint X))
Tactic: induction y using OnePoint.rec
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
x x_1 : X
⊢ (↑x : OnePoint X) ⤳ (↑x_1 : OnePoint X) ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 (↑x_1 : OnePoint X))
have coe : x ⤳ x_1 ∨ Disjoint (𝓝 x) (𝓝 x_1)
Tactic: rw [nhds_coe_eq, nhds_coe_eq, disjoint_map coe_injective, specializes_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Infinite X
inst_2 : DiscreteTopology X
⊢ ¬Continuous[_, instTopologicalSpace]
      (⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X)
have inhabit : ∀ (inhabited_h : Inhabited X),
  ¬Continuous[_, instTopologicalSpace]
      (⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X)
Tactic: inhabit X
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Infinite X
inst_2 : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Continuous[_, instTopologicalSpace]
      (⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X)
have simp : ∃ (x : CofiniteTopology (OnePoint X)),
  ¬Tendsto (β := OnePoint X)
      ((⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X) :
        (a : CofiniteTopology (OnePoint X)) → OnePoint X)
      (𝓝 x)
      (𝓝 ((Equiv.symm CofiniteTopology.of : (a : CofiniteTopology (OnePoint X)) → OnePoint X) x) : Filter (OnePoint X))
Tactic: simp only [continuous_iff_continuousAt, ContinuousAt, not_forall]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Infinite X
inst_2 : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ∃ (x : CofiniteTopology (OnePoint X)),
    ¬Tendsto (β := OnePoint X)
        ((⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X) :
          (a : CofiniteTopology (OnePoint X)) → OnePoint X)
        (𝓝 x)
        (𝓝 ((Equiv.symm CofiniteTopology.of : (a : CofiniteTopology (OnePoint X)) → OnePoint X) x) :
          Filter (OnePoint X))
have h : ¬Tendsto.{u_1, u_1} (α := CofiniteTopology (OnePoint X)) (β := OnePoint X)
    ((⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X) :
      (a : CofiniteTopology (OnePoint X)) → OnePoint X)
    (𝓝 ((CofiniteTopology.of : (a : OnePoint X) → CofiniteTopology (OnePoint X)) (↑default : OnePoint X)) :
      Filter (CofiniteTopology (OnePoint X)))
    (𝓝
        ((Equiv.symm CofiniteTopology.of : (a : CofiniteTopology (OnePoint X)) → OnePoint X)
          ((CofiniteTopology.of : (a : OnePoint X) → CofiniteTopology (OnePoint X)) (↑default : OnePoint X) :
            CofiniteTopology (OnePoint X))) :
      Filter (OnePoint X))
Tactic: use CofiniteTopology.of ↑(default : X)
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
h_1 : Membership.mem (γ := Set (OnePoint X)) univ ∞
hxy : ∞ ≠ y
⊢ ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
    IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ ∞ ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have infty : IsOpen[instTopologicalSpace] {y}
Tactic: refine ⟨{y}ᶜ, {y}, isOpen_compl_singleton, ?_, hxy, rfl, (compl_union_self _).symm.subset,
        disjoint_compl_left⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
h_1 : Membership.mem (γ := Set (OnePoint X)) univ ∞
hxy : ∞ ≠ y
⊢ IsOpen[instTopologicalSpace] {y}
have infty : IsOpen[inst_1] (some ⁻¹' {y})
Tactic: rw [OnePoint.isOpen_iff_of_notMem]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
h_1 : Membership.mem (γ := Set (OnePoint X)) univ ∞
hxy : ∞ ≠ y
infty : IsOpen[inst_1] (some ⁻¹' {y})
⊢ IsOpen[instTopologicalSpace] {y}
have infty₁ : ∞ ∉ {y}
Tactic: rw [OnePoint.isOpen_iff_of_notMem]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
val : X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ (↑val : OnePoint X)
hxy : (↑val : OnePoint X) ≠ y
⊢ ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
    IsOpen[instTopologicalSpace] u ∧
      IsOpen[instTopologicalSpace] v ∧ (↑val : OnePoint X) ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have coe : IsOpen[instTopologicalSpace] {(↑val : OnePoint X)}
Tactic: refine ⟨{some val}, {some val}ᶜ, ?_, isOpen_compl_singleton, rfl, hxy.symm, by simp,
        disjoint_compl_right⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
val : X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ (↑val : OnePoint X)
hxy : (↑val : OnePoint X) ≠ y
⊢ IsOpen[instTopologicalSpace] {(↑val : OnePoint X)}
have coe : IsOpen[inst_1] (some ⁻¹' {(↑val : OnePoint X)})
Tactic: rw [OnePoint.isOpen_iff_of_notMem]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
val : X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ (↑val : OnePoint X)
hxy : (↑val : OnePoint X) ≠ y
coe : IsOpen[inst_1] (some ⁻¹' {(↑val : OnePoint X)})
⊢ IsOpen[instTopologicalSpace] {(↑val : OnePoint X)}
have coe₁ : ∞ ∉ {(↑val : OnePoint X)}
Tactic: rw [OnePoint.isOpen_iff_of_notMem]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
x : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ x
y : OnePoint X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ y
hxy : x ≠ y
⊢ (fun (x y : OnePoint X) ↦
      ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
        IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v)
    x y
have infty : Membership.mem (γ := Set (OnePoint X)) univ ∞ →
  ∀ (hxy : ∞ ≠ y),
    ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
      IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ ∞ ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Tactic: cases x with
    | infty =>
      refine ⟨{y}ᶜ, {y}, isOpen_compl_singleton, ?_, hxy, rfl, (compl_union_self _).symm.subset,
        disjoint_compl_left⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, hxy]
    | coe val =>
      refine ⟨{some val}, {some val}ᶜ, ?_, isOpen_compl_singleton, rfl, hxy.symm, by simp,
        disjoint_compl_right⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, (Option.some_ne_none val).symm]
Cleared hypotheses: x, h, hxy
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
x : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ x
y : OnePoint X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ y
hxy : x ≠ y
infty :
  Membership.mem (γ := Set (OnePoint X)) univ ∞ →
    ∀ (hxy : ∞ ≠ y),
      ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
        IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ ∞ ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
⊢ ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
    IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have coe : ∀ (val : X),
  Membership.mem (γ := Set (OnePoint X)) univ (↑val : OnePoint X) →
    ∀ (hxy : (↑val : OnePoint X) ≠ y),
      ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
        IsOpen[instTopologicalSpace] u ∧
          IsOpen[instTopologicalSpace] v ∧ (↑val : OnePoint X) ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Tactic: cases x with
    | infty =>
      refine ⟨{y}ᶜ, {y}, isOpen_compl_singleton, ?_, hxy, rfl, (compl_union_self _).symm.subset,
        disjoint_compl_left⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, hxy]
    | coe val =>
      refine ⟨{some val}, {some val}ᶜ, ?_, isOpen_compl_singleton, rfl, hxy.symm, by simp,
        disjoint_compl_right⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, (Option.some_ne_none val).symm]
Cleared hypotheses: x, h, hxy
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
⊢ Tendsto f (coclosedCompact X) (𝓝 y)
have rw : ∀ t ∈ 𝓝 y, ∃ (i : Set X), IsCompact i ∧ MapsTo f iᶜ t
Tactic: rw [coclosedCompact_eq_cocompact, hasBasis_cocompact.tendsto_left_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
⊢ ∃ (i : Set X), IsCompact i ∧ MapsTo f iᶜ N
have obtain : ∀ (U : Set Y) (hU₁ : U ⊆ N) (hU₂ : IsOpen[inst_1] U) (hU₃ : y ∈ U), ∃ (i : Set X), IsCompact i ∧ MapsTo f iᶜ N
Tactic: obtain ⟨U, hU₁, hU₂, hU₃⟩ := mem_nhds_iff.mp hN
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst_1] U
hU₃ : y ∈ U
⊢ ∃ (i : Set X), IsCompact i ∧ MapsTo f iᶜ N
have refine : IsCompact (f ⁻¹' Uᶜ)
Tactic: refine ⟨f⁻¹' Uᶜ, ?_, by simpa using (mapsTo_preimage f U).mono_right hU₁⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst_1] U
hU₃ : y ∈ U
⊢ IsCompact (f ⁻¹' Uᶜ)
have rw : IsCompact Uᶜ
Tactic: rw [hf.isCompact_iff, image_preimage_eq_iff.mpr (by simpa [hy])]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
p : X
⊢ (fun (q : Y) ↦
        (if hq : q = y then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q) ⋯) : OnePoint X) : OnePoint X))
      ((fun (p : OnePoint X) ↦ p.elim y f) (↑p : OnePoint X)) =
    (↑p : OnePoint X)
have hp : f p ≠ y
Tactic: have hp : f p ≠ y := by simpa [hy] using mem_range_self (f := f) p