awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
hn : True
x : X × X
hx : x ∈ U n
refine_1 : (↑(d x.1 x.2) : ℝ) < (↑((1 / 2) ^ n) : ℝ)
refine_1₁ : d x.1 x.2 < (1 / 2) ^ n
⊢ (↑(d x.1 x.2) : ℝ) < (↑(1 / 2) : ℝ) ^ n
have refine_1₂ : ¬(1 / 2) ^ n ≤ d x.1 x.2
Tactic: rwa [← NNReal.coe_pow, NNReal.coe_lt_coe, ← not_le, hle_d, Classical.not_not]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
hn : True
x : X × X
hx : x ∈ U n
refine_1 : (↑(d x.1 x.2) : ℝ) < (↑((1 / 2) ^ n) : ℝ)
refine_1₁ : d x.1 x.2 < (1 / 2) ^ n
refine_1₂ : ¬(1 / 2) ^ n ≤ d x.1 x.2
⊢ (↑(d x.1 x.2) : ℝ) < (↑(1 / 2) : ℝ) ^ n
have refine_1₃ : ¬(x.1, x.2) ∉ U n
Tactic: rwa [← NNReal.coe_pow, NNReal.coe_lt_coe, ← not_le, hle_d, Classical.not_not]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
⊢ ∀ (i' : ℕ), True → ∃ (i : ℕ), True ∧ {p : X × X | dist p.1 p.2 < (↑(1 / 2) : ℝ) ^ i} ⊆ U i'
have refine_2 : ∀ (n : ℕ),
  True →
    ∀ (x : X × X) (hx : Membership.mem (γ := Set (X × X)) {p : X × X | dist p.1 p.2 < (↑(1 / 2) : ℝ) ^ (n + 1)} x),
      x ∈ U n
Tactic: refine fun n _ => ⟨n + 1, trivial, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (hypothesis)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
h : True
x : X × X
hx : Membership.mem (γ := Set (X × X)) {p : X × X | dist p.1 p.2 < (↑(1 / 2) : ℝ) ^ (n + 1)} x
⊢ x ∈ U n
have hx₁ : dist x.1 x.2 < (↑(1 / 2) : ℝ) ^ (n + 1)
Tactic: rw [mem_setOf_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
h : True
x : X × X
hx : dist x.1 x.2 < (↑(1 / 2) : ℝ) ^ (n + 1)
⊢ x ∈ U n
have refine_2 : ∀ (hx : x ∉ U n), (↑(1 / 2) : ℝ) ^ (n + 1) ≤ dist x.1 x.2
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
h : True
x : X × X
hx : x ∉ U n
⊢ (↑(1 / 2) : ℝ) ^ (n + 1) ≤ dist x.1 x.2
have refine_2 : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / 2
Tactic: refine le_trans ?_ ((div_le_iff₀' zero_lt_two).2 (hd_le x.1 x.2))
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
h : True
x : X × X
hx : x ∉ U n
⊢ (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / 2
have refine_2 : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / (↑2 : ℝ)
Tactic: rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ,
      mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
h : True
x : X × X
hx : x ∉ U n
refine_2 : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / (↑2 : ℝ)
⊢ (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / 2
have refine_2₁ : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2 / 2) : ℝ)
Tactic: rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ,
      mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
h : True
x : X × X
hx : x ∉ U n
refine_2 : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / (↑2 : ℝ)
refine_2₁ : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2 / 2) : ℝ)
⊢ (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / 2
have refine_2₂ : (↑((1 / 2) ^ (n + 1)) : ℝ) ≤ (↑(d x.1 x.2 / 2) : ℝ)
Tactic: rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ,
      mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
h : True
x : X × X
hx : x ∉ U n
refine_2 : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / (↑2 : ℝ)
refine_2₁ : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2 / 2) : ℝ)
refine_2₂ : (↑((1 / 2) ^ (n + 1)) : ℝ) ≤ (↑(d x.1 x.2 / 2) : ℝ)
⊢ (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / 2
have refine_2₃ : (1 / 2) ^ (n + 1) ≤ d x.1 x.2 / 2
Tactic: rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ,
      mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
h : True
x : X × X
hx : x ∉ U n
refine_2 : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / (↑2 : ℝ)
refine_2₁ : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2 / 2) : ℝ)
refine_2₂ : (↑((1 / 2) ^ (n + 1)) : ℝ) ≤ (↑(d x.1 x.2 / 2) : ℝ)
refine_2₃ : (1 / 2) ^ (n + 1) ≤ d x.1 x.2 / 2
⊢ (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / 2
have refine_2₄ : (1 / 2) ^ n * (1 / 2) ≤ d x.1 x.2 / 2
Tactic: rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ,
      mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
h : True
x : X × X
hx : x ∉ U n
refine_2 : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / (↑2 : ℝ)
refine_2₁ : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2 / 2) : ℝ)
refine_2₂ : (↑((1 / 2) ^ (n + 1)) : ℝ) ≤ (↑(d x.1 x.2 / 2) : ℝ)
refine_2₃ : (1 / 2) ^ (n + 1) ≤ d x.1 x.2 / 2
refine_2₄ : (1 / 2) ^ n * (1 / 2) ≤ d x.1 x.2 / 2
⊢ (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / 2
have refine_2₅ : (1 / 2) ^ n / 2 ≤ d x.1 x.2 / 2
Tactic: rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ,
      mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
h : True
x : X × X
hx : x ∉ U n
refine_2 : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / (↑2 : ℝ)
refine_2₁ : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2 / 2) : ℝ)
refine_2₂ : (↑((1 / 2) ^ (n + 1)) : ℝ) ≤ (↑(d x.1 x.2 / 2) : ℝ)
refine_2₃ : (1 / 2) ^ (n + 1) ≤ d x.1 x.2 / 2
refine_2₄ : (1 / 2) ^ n * (1 / 2) ≤ d x.1 x.2 / 2
refine_2₅ : (1 / 2) ^ n / 2 ≤ d x.1 x.2 / 2
⊢ (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / 2
have refine_2₆ : (1 / 2) ^ n ≤ d x.1 x.2 / 2 * 2
Tactic: rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ,
      mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
n : ℕ
h : True
x : X × X
hx : x ∉ U n
refine_2 : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / (↑2 : ℝ)
refine_2₁ : (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2 / 2) : ℝ)
refine_2₂ : (↑((1 / 2) ^ (n + 1)) : ℝ) ≤ (↑(d x.1 x.2 / 2) : ℝ)
refine_2₃ : (1 / 2) ^ (n + 1) ≤ d x.1 x.2 / 2
refine_2₄ : (1 / 2) ^ n * (1 / 2) ≤ d x.1 x.2 / 2
refine_2₅ : (1 / 2) ^ n / 2 ≤ d x.1 x.2 / 2
refine_2₆ : (1 / 2) ^ n ≤ d x.1 x.2 / 2 * 2
⊢ (↑(1 / 2) : ℝ) ^ (n + 1) ≤ (↑(d x.1 x.2) : ℝ) / 2
have refine_2₇ : (1 / 2) ^ n ≤ d x.1 x.2
Tactic: rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ,
      mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]
-- 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
⊢ ∃ (f : X → ℕ →ᵇ ℝ), IsInducing f
have rcases : ∀ (B : Set (Set X)) (hBc : B.Countable) (hB : IsTopologicalBasis B), ∃ (f : X → ℕ →ᵇ ℝ), IsInducing f
Tactic: rcases exists_countable_basis X with ⟨B, hBc, -, hB⟩
-- 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}
⊢ ∃ (f : X → ℕ →ᵇ ℝ), IsInducing f
have haveI : ∀ (this : Encodable (↑s : Type u_1)), ∃ (f : X → ℕ →ᵇ ℝ), IsInducing f
Tactic: haveI : Encodable s := ((hBc.prod hBc).mono (sep_subset _ _)).toEncodable
-- 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 : TopologicalSpace (↑s : Type u_1) := ⊥
⊢ ∃ (f : X → ℕ →ᵇ ℝ), IsInducing f
have this₁ : DiscreteTopology.{u_1} (↑s : Type u_1)
Tactic: haveI : DiscreteTopology s := ⟨rfl⟩
-- 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)
⊢ ∃ (f : X → ℕ →ᵇ ℝ), IsInducing f
have rsuffices : ∀ (f : X → (↑s : Type u_1) →ᵇ ℝ) (hf : IsInducing f), ∃ (f : X → ℕ →ᵇ ℝ), IsInducing f
Tactic: rsuffices ⟨f, hf⟩ : ∃ f : X → s →ᵇ ℝ, IsInducing f
-- 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)
rsuffices : ∀ (f : X → (↑s : Type u_1) →ᵇ ℝ) (hf : IsInducing f), ∃ (f : X → ℕ →ᵇ ℝ), IsInducing f
⊢ ∃ (f : X → ℕ →ᵇ ℝ), IsInducing f
have rsuffices₁ : ∃ (f : X → (↑s : Type u_1) →ᵇ ℝ), IsInducing f
Tactic: rsuffices ⟨f, hf⟩ : ∃ f : X → s →ᵇ ℝ, IsInducing f
-- 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)
⊢ ∃ (f : X → (↑s : Type u_1) →ᵇ ℝ), IsInducing f
have hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
Tactic: have hd : ∀ UV : s, Disjoint (closure UV.1.1) UV.1.2ᶜ :=
    fun UV => disjoint_compl_right.mono_right (compl_subset_compl.2 UV.2.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) → ℝ),
    (∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)) ∧ Tendsto ε cofinite (𝓝 0)
have rcases : ∀ (ε : (↑s : Type u_1) → ℝ) (ε0 : ∀ (i : (↑s : Type u_1)), 0 < ε i) (c : ℝ) (hεc : HasSum ε c) (hc1 : c ≤ 1),
  ∃ (ε : (↑s : Type u_1) → ℝ),
    (∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)) ∧ Tendsto ε cofinite (𝓝 0)
Tactic: rcases posSumOfEncodable zero_lt_one s with ⟨ε, ε0, c, hεc, hc1⟩
-- 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) → ℝ
ε0 : ∀ (i : (↑s : Type u_1)), 0 < ε i
c : ℝ
hεc : HasSum ε c
hc1 : c ≤ 1
⊢ ∃ (ε : (↑s : Type u_1) → ℝ),
    (∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)) ∧ Tendsto ε cofinite (𝓝 0)
have refine : ∀ (UV : (↑s : Type u_1)), ε UV ≤ 1
Tactic: refine ⟨ε, fun UV => ⟨ε0 UV, ?_⟩, hεc.summable.tendsto_cofinite_zero⟩
-- 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ᶜ
⊢ ∃ (f : X → (↑s : Type u_1) →ᵇ ℝ), IsInducing f
have obtain : ∀ (ε : (↑s : Type u_1) → ℝ) (ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV))
  (hε : Tendsto ε cofinite (𝓝 0)), ∃ (f : X → (↑s : Type u_1) →ᵇ ℝ), IsInducing f
Tactic: obtain ⟨ε, ε01, hε⟩ : ∃ ε : s → ℝ, (∀ UV, ε UV ∈ Ioc (0 : ℝ) 1) ∧ Tendsto ε cofinite (𝓝 0) := by
    rcases posSumOfEncodable zero_lt_one s with ⟨ε, ε0, c, hεc, hc1⟩
    refine ⟨ε, fun UV => ⟨ε0 UV, ?_⟩, hεc.summable.tendsto_cofinite_zero⟩
    exact (le_hasSum hεc UV fun _ _ => (ε0 _).le).trans hc1