awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Metrizable.Uniformity
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)
⊢ (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:
⟨x₂, h₁₂, x₃, h₂₃, h₃₄⟩

Premises used: Set.Mem, setOf, SetRel.comp, And.intro, Exists.intro
-- Module: Mathlib.Topology.Metrizable.Uniformity
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)
⊢ (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:
exact ⟨x₂, h₁₂, x₃, h₂₃, h₃₄⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))

Tactic:
(dif_neg H).trans_le zero_le

Premises used: zero_le, Eq.trans_le, dif_neg
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))

Tactic:
exact (dif_neg H).trans_le zero_le

Premises used: Eq.trans_le, dif_neg
-- Module: Mathlib.Topology.Metrizable.Uniformity
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

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
-- Module: Mathlib.Topology.Metrizable.Uniformity
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
⊢ (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)

Tactic:
rw [mem_Ioo, ← NNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hr

Premises used: Set.mem_Ioo, NNReal.coe_lt_coe
-- Module: Mathlib.Topology.Metrizable.Uniformity
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
hr₁ : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
⊢ let I := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm;
  ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)

Tactic:
rw [mem_Ioo, ← NNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hr

Premises used: Set.mem_Ioo, NNReal.coe_lt_coe
-- Module: Mathlib.Topology.Metrizable.Uniformity
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
hr₁ : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
hdist_le₁ :
  let I := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm;
  ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
⊢ ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n

Tactic:
rw [mem_Ioo, ← NNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hr

Premises used: Set.mem_Ioo, NNReal.coe_lt_coe
-- Module: Mathlib.Topology.Metrizable.Uniformity
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
hr₁ : (↑0 : ℝ) < (↑(1 / 2) : ℝ) ∧ (↑(1 / 2) : ℝ) < (↑1 : ℝ)
hdist_le₁ :
  let I := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm;
  ∀ (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
⊢ let I := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm;
  ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y

Tactic:
rw [mem_Ioo, ← NNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hr

Premises used: Set.mem_Ioo, NNReal.coe_lt_coe
-- Module: Mathlib.Topology.Metrizable.Uniformity
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

Tactic:
⟨I, UniformSpace.ext <| (uniformity_basis_dist_pow hr.1 hr.2).ext hB.toHasBasis ?_ ?_⟩

Premises used: Filter.HasAntitoneBasis.toHasBasis, UniformSpace.ext, Metric.uniformity_basis_dist_pow, And.right, And.left, Exists.intro, Filter.HasBasis.ext
-- Module: Mathlib.Topology.Metrizable.Uniformity
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}
refine_2 : ∀ (i' : ℕ), True → ∃ (i : ℕ), True ∧ {p : X × X | dist p.1 p.2 < (↑(1 / 2) : ℝ) ^ i} ⊆ U i'
⊢ ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst

Tactic:
refine ⟨I, UniformSpace.ext <| (uniformity_basis_dist_pow hr.1 hr.2).ext hB.toHasBasis ?_ ?_⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
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}

Tactic:
fun n hn => ⟨n, hn, fun x hx => (hdist_le _ _).trans_lt ?_⟩

Premises used: Prod.fst, And.intro, Exists.intro, LE.le.trans_lt, Prod.snd
-- Module: Mathlib.Topology.Metrizable.Uniformity
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 : ∀ (n : ℕ) (hn : True) (x : X × X) (hx : x ∈ U n), (↑(d x.1 x.2) : ℝ) < (↑(1 / 2) : ℝ) ^ n
⊢ ∀ (i : ℕ), True → ∃ (i' : ℕ), True ∧ U i' ⊆ {p : X × X | dist p.1 p.2 < (↑(1 / 2) : ℝ) ^ i}

Tactic:
refine fun n hn => ⟨n, hn, fun x hx => (hdist_le _ _).trans_lt ?_⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
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
refine_1₃ : ¬(x.1, x.2) ∉ U n
refine_1₄ refine_1₅ refine_1₆ refine_1₇ : (x.1, x.2) ∈ U n
⊢ (↑(d x.1 x.2) : ℝ) < (↑(1 / 2) : ℝ) ^ n

Tactic:
rwa [← NNReal.coe_pow, NNReal.coe_lt_coe, ← not_le, hle_d, Classical.not_not]

Premises used: not_le, Classical.not_not, NNReal.coe_pow, NNReal.coe_lt_coe
-- Module: Mathlib.Topology.Metrizable.Uniformity
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'

Tactic:
fun n _ => ⟨n + 1, trivial, fun x hx => ?_⟩

Premises used: trivial, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Metrizable.Uniformity
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_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
⊢ ∀ (i' : ℕ), True → ∃ (i : ℕ), True ∧ {p : X × X | dist p.1 p.2 < (↑(1 / 2) : ℝ) ^ i} ⊆ U i'

Tactic:
refine fun n _ => ⟨n + 1, trivial, fun x hx => ?_⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
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
⊢ dist x.1 x.2 < (↑(1 / 2) : ℝ) ^ (n + 1)

Tactic:
rw [mem_setOf_eq] at hx

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Topology.Metrizable.Uniformity
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)
refine_2 : ∀ (hx : x ∉ U n), (↑(1 / 2) : ℝ) ^ (n + 1) ≤ dist x.1 x.2
⊢ x ∈ U n

Tactic:
contrapose! hx
-- Module: Mathlib.Topology.Metrizable.Uniformity
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

Tactic:
le_trans ?_ ((div_le_iff₀' zero_lt_two).2 (hd_le x.1 x.2))

Premises used: Iff.mpr, Prod.fst, div_le_iff₀', Prod.snd, le_trans
-- Module: Mathlib.Topology.Metrizable.Uniformity
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) ≤ dist x.1 x.2

Tactic:
refine le_trans ?_ ((div_le_iff₀' zero_lt_two).2 (hd_le x.1 x.2))

Premises used: Iff.mpr, Prod.fst, div_le_iff₀', Prod.snd, le_trans
-- Module: Mathlib.Topology.Metrizable.Uniformity
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
refine_2₇ : (1 / 2) ^ n ≤ d x.1 x.2
refine_2₈ refine_2₉ refine_2₁₀ refine_2₁₁ : (x.1, x.2) ∉ U n
⊢ (↑(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]

Premises used: div_le_iff₀, div_mul_cancel₀, NNReal.coe_div, pow_succ, NNReal.coe_two, two_ne_zero, mul_one_div, NNReal.coe_pow, NNReal.coe_le_coe
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
inst_2 : T0Space X
⊢ TopologicalSpace.MetrizableSpace X

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X_1 : Type u_1
X : Type u_2
t : TopologicalSpace X
inst : TopologicalSpace.PseudoMetrizableSpace X
⊢ PseudoMetricSpace.toUniformSpace = TopologicalSpace.pseudoMetrizableSpaceUniformity X

Tactic:
rfl
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X_1 : Type u_1
X : Type u_2
t : TopologicalSpace X
inst : TopologicalSpace.PseudoMetrizableSpace X
⊢ PseudoMetricSpace.toUniformSpace = TopologicalSpace.pseudoMetrizableSpaceUniformity X

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X_1 : Type u_1
X : Type u_2
t : TopologicalSpace X
inst : TopologicalSpace.MetrizableSpace X
⊢ MetricSpace.toPseudoMetricSpace = TopologicalSpace.pseudoMetrizableSpacePseudoMetric X

Tactic:
rfl