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
x y : X
pos :
  ∀ (h : ∃ (n : ℕ), (x, y) ∉ U n), (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i
⊢ Eq (α := ℝ≥0) (if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0) 0 ↔
    ∀ (i : ℕ), (x, y) ∈ U i
have neg : ∀ (h : ¬∃ (n : ℕ), (x, y) ∉ U n), Eq (α := ℝ≥0) 0 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i
Tactic: split_ifs with h
-- 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
⊢ ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst
have hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
Tactic: have hd₀ : ∀ {x y}, d x y = 0 ↔ Inseparable x y := by
    intro x y
    refine Iff.trans ?_ hB.inseparable_iff_uniformity.symm
    simp only [d, true_imp_iff]
    split_ifs with h
    · simp [h, pow_eq_zero_iff']
    · simpa only [not_exists, Classical.not_not, eq_self_iff_true, true_iff] using h
-- 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
⊢ ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst
have hd_symm : ∀ (x y : X), d x y = d y x
Tactic: have hd_symm x y : d x y = d y x := by simp only [d, (U _).comm]
-- 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
⊢ ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst
have hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
Tactic: have hr : (1 / 2 : ℝ≥0) ∈ Ioo (0 : ℝ≥0) 1 := ⟨half_pos one_pos, NNReal.half_lt_self one_ne_zero⟩
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
⊢ ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst
have hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
Tactic: have hdist_le : ∀ x y, dist x y ≤ d x y := PseudoMetricSpace.dist_ofPreNNDist_le _ _ _
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
x y : X
n : ℕ
⊢ ((1 / 2) ^ n ≤ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0) ↔
    (x, y) ∉ U n
have pos : ∀ (h : ∃ (n : ℕ), (x, y) ∉ U n), (1 / 2) ^ n ≤ (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h ↔ (x, y) ∉ U n
Tactic: split_ifs with h
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
x y : X
n : ℕ
pos :
  ∀ (h : ∃ (n : ℕ), (x, y) ∉ U n), (1 / 2) ^ n ≤ (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h ↔ (x, y) ∉ U n
⊢ ((1 / 2) ^ n ≤ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0) ↔
    (x, y) ∉ U n
have neg : ∀ (h : ¬∃ (n : ℕ), (x, y) ∉ U n), (1 / 2) ^ n ≤ 0 ↔ (x, y) ∉ U n
Tactic: split_ifs with h
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
x y : X
n : ℕ
h : ∃ (n : ℕ), (x, y) ∉ U n
⊢ (1 / 2) ^ n ≤ (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h ↔ (x, y) ∉ U n
have pos : (∃ m ≤ n, (x, y) ∉ U m) ↔ (x, y) ∉ U n
Tactic: rw [(pow_right_strictAnti₀ hr.1 hr.2).le_iff_ge, Nat.find_le_iff]
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
x y : X
n : ℕ
h : ¬∃ (n : ℕ), (x, y) ∉ U n
⊢ (1 / 2) ^ n ≤ 0 ↔ (x, y) ∉ U n
have h₁ : ∀ (n : ℕ), (x, y) ∈ U n
Tactic: push Not at h
Cleared hypotheses: h
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
⊢ ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst
have hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
Tactic: have hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n := by
    intro x y n
    dsimp only [d]
    split_ifs with h
    · rw [(pow_right_strictAnti₀ hr.1 hr.2).le_iff_ge, Nat.find_le_iff]
      exact ⟨fun ⟨m, hmn, hm⟩ hn => hm (hB.antitone hmn hn), fun h => ⟨n, le_rfl, h⟩⟩
    · push Not at h
      simp only [h, not_true, (pow_pos hr.1 _).not_ge]
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
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
⊢ ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
have refine : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
Tactic: refine PseudoMetricSpace.le_two_mul_dist_ofPreNNDist _ _ _ fun x₁ x₂ x₃ x₄ => ?_
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
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
x₁ x₂ x₃ x₄ : X
⊢ d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
have pos : ∀ (H : ∃ (n : ℕ), (x₁, x₄) ∉ U n), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
Tactic: by_cases H : ∃ n, (x₁, x₄) ∉ U n
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
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
x₁ x₂ x₃ x₄ : X
pos : ∀ (H : ∃ (n : ℕ), (x₁, x₄) ∉ U n), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
⊢ d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
have neg : ∀ (H : ¬∃ (n : ℕ), (x₁, x₄) ∉ U n), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
Tactic: by_cases H : ∃ n, (x₁, x₄) ∉ U n
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
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
x₁ x₂ x₃ x₄ : X
H : ∃ (n : ℕ), (x₁, x₄) ∉ U n
⊢ d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
have pos : (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
Tactic: refine (dif_pos H).trans_le ?_
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
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
x₁ x₂ x₃ x₄ : X
H : ∃ (n : ℕ), (x₁, x₄) ∉ U n
⊢ (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
have pos : (1 / 2) ^ (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ≤ max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
Tactic: rw [← div_le_iff₀' zero_lt_two, ← mul_one_div (_ ^ _), ← pow_succ]
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
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
x₁ x₂ x₃ x₄ : X
H : ∃ (n : ℕ), (x₁, x₄) ∉ U n
⊢ (1 / 2) ^ (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ≤ max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
have pos : ¬((x₁, x₂) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ∧
    (x₂, x₃) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ∧
      (x₃, x₄) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1))
Tactic: simp only [le_max_iff, hle_d, ← not_and_or]
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
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
x₁ x₂ x₃ x₄ : X
H : ∃ (n : ℕ), (x₁, x₄) ∉ U n
h₁₂ : (x₁, x₂) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1)
h₂₃ : (x₂, x₃) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1)
h₃₄ : (x₃, x₄) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1)
⊢ False
have pos : (x₁, x₄) ∈
  U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ○
    (U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ○ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1))
Tactic: refine Nat.find_spec H (hU_comp (lt_add_one <| Nat.find H) ?_)
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
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
⊢ ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst
have hd_le : ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y
Tactic: have hd_le : ∀ x y, ↑(d x y) ≤ 2 * dist x y := by
    refine PseudoMetricSpace.le_two_mul_dist_ofPreNNDist _ _ _ fun x₁ x₂ x₃ x₄ => ?_
    by_cases H : ∃ n, (x₁, x₄) ∉ U n
    · refine (dif_pos H).trans_le ?_
      rw [← div_le_iff₀' zero_lt_two, ← mul_one_div (_ ^ _), ← pow_succ]
      simp only [le_max_iff, hle_d, ← not_and_or]
      rintro ⟨h₁₂, h₂₃, h₃₄⟩
      refine Nat.find_spec H (hU_comp (lt_add_one <| Nat.find H) ?_)
      exact ⟨x₂, h₁₂, x₃, h₂₃, h₃₄⟩
    · exact (dif_neg H).trans_le zero_le
-- 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 : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
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 : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst
have hr₁ : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
Tactic: rw [mem_Ioo, ← NNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hr
Cleared hypotheses: hr, I, hdist_le, hle_d, hd_le
-- 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 : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst
have refine_1 : ∀ (i : ℕ), True → ∃ (i' : ℕ), True ∧ U i' ⊆ {p : X × X | dist p.1 p.2 < (↑(1 / 2) : ℝ) ^ i}
Tactic: refine ⟨I, UniformSpace.ext <| (uniformity_basis_dist_pow hr.1 hr.2).ext hB.toHasBasis ?_ ?_⟩
-- 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
refine_1 : ∀ (i : ℕ), True → ∃ (i' : ℕ), True ∧ U i' ⊆ {p : X × X | dist p.1 p.2 < (↑(1 / 2) : ℝ) ^ i}
⊢ ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst
have refine_2 : ∀ (i' : ℕ), True → ∃ (i : ℕ), True ∧ {p : X × X | dist p.1 p.2 < (↑(1 / 2) : ℝ) ^ i} ⊆ U i'
Tactic: refine ⟨I, UniformSpace.ext <| (uniformity_basis_dist_pow hr.1 hr.2).ext hB.toHasBasis ?_ ?_⟩
-- 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 ∧ U i' ⊆ {p : X × X | dist p.1 p.2 < (↑(1 / 2) : ℝ) ^ i}
have refine_1 : ∀ (n : ℕ) (hn : True) (x : X × X) (hx : x ∈ U n), (↑(d x.1 x.2) : ℝ) < (↑(1 / 2) : ℝ) ^ n
Tactic: refine fun n hn => ⟨n, hn, fun x hx => (hdist_le _ _).trans_lt ?_⟩
-- 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
⊢ (↑(d x.1 x.2) : ℝ) < (↑(1 / 2) : ℝ) ^ n
have refine_1 : (↑(d x.1 x.2) : ℝ) < (↑((1 / 2) ^ 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
n : ℕ
hn : True
x : X × X
hx : x ∈ U n
refine_1 : (↑(d x.1 x.2) : ℝ) < (↑((1 / 2) ^ n) : ℝ)
⊢ (↑(d x.1 x.2) : ℝ) < (↑(1 / 2) : ℝ) ^ n
have refine_1₁ : d x.1 x.2 < (1 / 2) ^ n
Tactic: rwa [← NNReal.coe_pow, NNReal.coe_lt_coe, ← not_le, hle_d, Classical.not_not]