awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this_3 : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
δ : ℝ
δ0 : 0 < δ
h_fin : Set.Finite.{u_1} (α := (↑s : Type u_1)) {UV : (↑s : Type u_1) | δ ≤ ε UV}
this :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (UV : (↑s : Type u_1)),
      δ ≤ ε UV → dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
y : X
hy :
  ∀ (UV : (↑s : Type u_1)),
    δ ≤ ε UV → dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
UV : (↑s : Type u_1)
refine_1 :
  ∀ (hle : δ ≤ ε UV),
    dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
⊢ dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
have refine_1₁ : ∀ (hle : ε UV ≤ δ),
  dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
Tactic: rcases le_total δ (ε UV) with hle | hle
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
⊢ comap F (𝓝 (F x)) ≤ 𝓝 x
have refine_2 : ∀ (i' : Set X), i' ∈ B ∧ x ∈ i' → ∃ (i : ℝ), 0 < i ∧ F ⁻¹' ball (F x) i ⊆ i'
Tactic: refine ((nhds_basis_ball.comap _).le_basis_iff hB.nhds_hasBasis).2 ?_
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
⊢ ∃ (i : ℝ), 0 < i ∧ F ⁻¹' ball (F x) i ⊆ V
have refine_2 : ∀ (U : Set X) (hUB : U ∈ B) (hxU : x ∈ U) (hUV : closure[inst] U ⊆ V), ∃ (i : ℝ), 0 < i ∧ F ⁻¹' ball (F x) i ⊆ V
Tactic: rcases hB.exists_closure_subset (hB.mem_nhds hVB hxV) with ⟨U, hUB, hxU, hUV⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst] U ⊆ V
UV : (↑s : Type u_1) := Subtype.mk (p := fun (x : Set X × Set X) ↦ x ∈ s) (U, V) ⋯
⊢ ∃ (i : ℝ), 0 < i ∧ F ⁻¹' ball (F x) i ⊆ V
have refine_2 : ∀ (y : X) (hy : dist (F y) (F x) < ε UV), y ∈ V
Tactic: refine ⟨ε UV, (ε01 UV).1, fun y (hy : dist (F y) (F x) < ε UV) => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst] U ⊆ V
UV : (↑s : Type u_1) := Subtype.mk (p := fun (x : Set X × Set X) ↦ x ∈ s) (U, V) ⋯
y : X
hy : dist (F y) (F x) < ε UV
⊢ y ∈ V
have hy₁ : dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) < ε UV
Tactic: replace hy : dist (F y UV) (F x UV) < ε UV :=
      (BoundedContinuousFunction.dist_coe_le_dist _).trans_lt hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst] U ⊆ V
UV : (↑s : Type u_1) := Subtype.mk (p := fun (x : Set X × Set X) ↦ x ∈ s) (U, V) ⋯
y : X
hy : dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) < ε UV
⊢ y ∈ V
have refine_2 : ∀ (hy : ¬y ∈ V),
  ε UV ≤ dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ)
Tactic: contrapose! hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst] U ⊆ V
UV : (↑s : Type u_1) := Subtype.mk (p := fun (x : Set X × Set X) ↦ x ∈ s) (U, V) ⋯
y : X
hy : ¬y ∈ V
⊢ ε UV ≤ dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ)
have refine_2 : ε UV ≤ norm (E := ℝ) ((fun (x : X) ↦ ε UV) y)
Tactic: rw [hF, hF, hfε UV hy, hf0 UV hxU, Pi.zero_apply, dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
this : ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
have rcases : ∀ (U : ℕ → Set X) (hne : ∀ (n : ℕ), (U n).Nonempty) (ho : ∀ (n : ℕ), IsOpen[inst] (U n))
  (hd : Pairwise (Disjoint on U)),
  ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
Tactic: rcases this with ⟨U, hne, ho, hd⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
have refine_1 : ∀ (n : ℕ), Set.Infinite.{u_1} (α := X) ((fun (n : ℕ) ↦ (⋃ (m : ℕ), U (Nat.pair n m) : Set X)) n)
Tactic: refine ⟨fun n ↦ ⋃ m, U (.pair n m), ?_, fun _ ↦ isOpen_iUnion fun _ ↦ ho _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
refine_1 : ∀ (n : ℕ), Set.Infinite.{u_1} (α := X) ((fun (n : ℕ) ↦ (⋃ (m : ℕ), U (Nat.pair n m) : Set X)) n)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
have refine_2 : Pairwise (α := ℕ) (onFun.{1, u_1 + 1, 1} (β := Set X) Disjoint fun (n : ℕ) ↦ ⋃ (m : ℕ), U (Nat.pair n m))
Tactic: refine ⟨fun n ↦ ⋃ m, U (.pair n m), ?_, fun _ ↦ isOpen_iUnion fun _ ↦ ho _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
⊢ ∀ (n : ℕ), Set.Infinite.{u_1} (α := X) ((fun (n : ℕ) ↦ (⋃ (m : ℕ), U (Nat.pair n m) : Set X)) n)
have refine_1 : ∀ (n i j : ℕ) (hij : U (Nat.pair n i) = U (Nat.pair n j)), i = j
Tactic: refine fun n ↦ infinite_iUnion fun i j hij ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
n i j : ℕ
hij : U (Nat.pair n i) = U (Nat.pair n j)
⊢ i = j
have refine_1 : Nat.pair n i = Nat.pair n j
Tactic: suffices n.pair i = n.pair j by simpa
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
n i j : ℕ
hij : U (Nat.pair n i) = U (Nat.pair n j)
⊢ Nat.pair n i = Nat.pair n j
have refine_1 : ¬(Disjoint on U) (Nat.pair n i) (Nat.pair n j)
Tactic: apply hd.eq
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
⊢ Pairwise (α := ℕ) (onFun.{1, u_1 + 1, 1} (β := Set X) Disjoint fun (n : ℕ) ↦ ⋃ (m : ℕ), U (Nat.pair n m))
have refine_2 : ∀ (n n' : ℕ) (hne : n ≠ n') (m m' : ℕ), Nat.pair n m ≠ Nat.pair n' m'
Tactic: refine fun n n' hne ↦ disjoint_iUnion_left.2 fun m ↦ disjoint_iUnion_right.2 fun m' ↦ hd ?_
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
have suffices : ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
Tactic: suffices ∃ U : ℕ → Set X, (∀ n, (U n).Nonempty) ∧ (∀ n, IsOpen (U n)) ∧
      Pairwise (Disjoint on U) by
    rcases this with ⟨U, hne, ho, hd⟩
    refine ⟨fun n ↦ ⋃ m, U (.pair n m), ?_, fun _ ↦ isOpen_iUnion fun _ ↦ ho _, ?_⟩
    · refine fun n ↦ infinite_iUnion fun i j hij ↦ ?_
      suffices n.pair i = n.pair j by simpa
      apply hd.eq
      simpa [hij, onFun] using (hne _).ne_empty
    · refine fun n n' hne ↦ disjoint_iUnion_left.2 fun m ↦ disjoint_iUnion_right.2 fun m' ↦ hd ?_
      simp [hne]
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
have pos : ∀ (h : DiscreteTopology X),
  ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
Tactic: by_cases h : DiscreteTopology X
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
pos :
  ∀ (h : DiscreteTopology X),
    ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
have neg : ∀ (h : ¬DiscreteTopology X),
  ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
Tactic: by_cases h : DiscreteTopology X
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
h : DiscreteTopology X
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
have pos : ∀ (x x_1 : ℕ) (h : x ≠ x_1),
  onFun.{1, u_1 + 1, 1} (β := Set X) Disjoint
    (fun (n : ℕ) ↦ singleton (α := X) ((Infinite.natEmbedding X : (a : ℕ) → X) n : X)) x x_1
Tactic: refine ⟨fun n ↦ {Infinite.natEmbedding X n}, fun _ ↦ singleton_nonempty _,
      fun _ ↦ isOpen_discrete _, fun _ _ h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
h : ¬DiscreteTopology X
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
have h₁ : ∃ (x : X), (𝓝[≠] x).NeBot
Tactic: simp only [discreteTopology_iff_nhds_ne, not_forall, ← ne_eq, ← neBot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
h : ∃ (x : X), (𝓝[≠] x).NeBot
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
have neg : ∀ (x : X) (hx : (𝓝[≠] x).NeBot),
  ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
Tactic: rcases h with ⟨x, hx⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this : ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧ Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
have rcases : ∀ (U : ℕ → Set X) (hU : ∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x) (hd : Pairwise (Disjoint on U)),
  ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
Tactic: rcases this with ⟨U, hU, hd⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
have neg : ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧ Pairwise (Disjoint on U)
Tactic: suffices ∃ U : ℕ → Set X, (∀ n, (U n).Nonempty ∧ IsOpen (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧
        Pairwise (Disjoint on U) by
      rcases this with ⟨U, hU, hd⟩
      exact ⟨U, fun n ↦ (hU n).1, fun n ↦ (hU n).2.1, hd⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧ Pairwise (Disjoint on U)
have this : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
Tactic: have : Std.Symm (α := Set X) Disjoint := ⟨fun _ _ h ↦ h.symm⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧ Pairwise (Disjoint on U)
have neg : ∀ (S : Finset (Set X)) (hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1),
  ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
Tactic: refine exists_seq_of_forall_finset_exists' (fun U : Set X ↦ U.Nonempty ∧ IsOpen U ∧ Uᶜ ∈ 𝓝 x)
      Disjoint fun S hS ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
⊢ ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
have this₁ : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
Tactic: have : (⋂ U ∈ S, interior (Uᶜ)) \ {x} ∈ 𝓝[≠] x := inter_mem_inf ((biInter_finset_mem _).2
      fun U hU ↦ interior_mem_nhds.2 (hS _ hU).2.2) (mem_principal_self _)
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
⊢ ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
have neg : ∀ (y : X) (hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y) (hyx : y ≠ x),
  ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
Tactic: rcases hx.nonempty_of_mem this with ⟨y, hyU, hyx : y ≠ x⟩