-- Mathlib/Topology/Metrizable/Uniformity.lean
theorem UniformSpace.metrizable_uniformity (X : Type*) [UniformSpace X]
    [IsCountablyGenerated (𝓤 X)] : ∃ I : PseudoMetricSpace X, I.toUniformSpace = ‹_›

Proof state:
case intro.intro.intro
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
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 => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find 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 : 1 / 2 ∈ Ioo 0 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.toUniformSpace = inst✝¹

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

Result:
case intro.intro.intro
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
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 => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find 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.toUniformSpace = inst✝¹

Proof state:
case intro.intro.intro.refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
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 => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find 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 : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ ↑(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))

Result:
case intro.intro.intro.refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
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 => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find 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 : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ ↑(1 / 2) ^ (n + 1) ≤ ↑(d x.1 x.2) / 2

Proof state:
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
⊢ ∃ U, (∀ (n : ℕ), SymmetricRel (U n)) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U

Tactic:
rcases UniformSpace.has_seq_basis X with ⟨V, hB, hV_symm⟩

Result:
case intro.intro
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
V : ℕ → Set (X × X)
hB : (𝓤 X).HasAntitoneBasis V
hV_symm : ∀ (n : ℕ), SymmetricRel (V n)
⊢ ∃ U, (∀ (n : ℕ), SymmetricRel (U n)) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U

Proof state:
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
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 => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find 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 : 1 / 2 ∈ Ioo 0 1
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 ≤ d x y ↔ (x, y) ∉ U n

Tactic:
intro x y n

Result:
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
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 => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find 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 : 1 / 2 ∈ Ioo 0 1
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 ≤ d x y ↔ (x, y) ∉ U n

Proof state:
case intro.intro.intro
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
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 => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find 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.toUniformSpace = inst✝¹

Tactic:
have hr : (1 / 2 : ℝ≥0) ∈ Ioo (0 : ℝ≥0) 1 := ⟨half_pos one_pos, NNReal.half_lt_self one_ne_zero⟩

Result:
case intro.intro.intro
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
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 => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find 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 : 1 / 2 ∈ Ioo 0 1
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹

Proof state:
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
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 => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
⊢ ∀ {x y : X}, d x y = 0 ↔ Inseparable x y

Tactic:
intro x y

Result:
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
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 => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
x y : X
⊢ d x y = 0 ↔ Inseparable x y