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

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:
dsimp only [d]

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 ≤ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0) ↔ (x, y) ∉ U n

Proof state:
case pos
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
x₁ x₂ x₃ x₄ : X
H : ∃ n, (x₁, x₄) ∉ U n
⊢ (1 / 2) ^ Nat.find H ≤ 2 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))

Tactic:
rw [← div_le_iff₀' zero_lt_two, ← mul_one_div (_ ^ _), ← pow_succ]

Result:
case pos
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
x₁ x₂ x₃ x₄ : X
H : ∃ n, (x₁, x₄) ∉ U n
⊢ (1 / 2) ^ (Nat.find H + 1) ≤ d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄)

Proof state:
case pos
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
x₁ x₂ x₃ x₄ : X
H : ∃ n, (x₁, x₄) ∉ U n
⊢ ¬((x₁, x₂) ∈ U (Nat.find H + 1) ∧ (x₂, x₃) ∈ U (Nat.find H + 1) ∧ (x₃, x₄) ∈ U (Nat.find H + 1))

Tactic:
rintro ⟨h₁₂, h₂₃, h₃₄⟩

Result:
case pos.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
x₁ x₂ x₃ x₄ : X
H : ∃ n, (x₁, x₄) ∉ U n
h₁₂ : (x₁, x₂) ∈ U (Nat.find H + 1)
h₂₃ : (x₂, x₃) ∈ U (Nat.find H + 1)
h₃₄ : (x₃, x₄) ∈ U (Nat.find H + 1)
⊢ False

Proof state:
case neg
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
x₁ x₂ x₃ x₄ : X
H : ¬∃ n, (x₁, x₄) ∉ U n
⊢ d x₁ x₄ ≤ 2 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))

Tactic:
exact (dif_neg H).trans_le (zero_le _)

Result:
no goals

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
x y : X
⊢ d x y = d y x

Tactic:
simp only [d, @SymmetricRel.mk_mem_comm _ _ (hU_symm _) x y]

Result:
no goals

Proof state:
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

Tactic:
rcases hB.subbasis_with_rel fun m =>
    hB.tendsto_smallSets.eventually
      (eventually_uniformity_iterate_comp_subset (hB.mem m) 2) with
  ⟨φ, -, hφ_comp, hφB⟩

Result:
case intro.intro.intro.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)
φ : ℕ → ℕ
hφ_comp : ∀ ⦃m n : ℕ⦄, m < n → (fun x => V (φ n) ○ x)^[2] (V (φ n)) ⊆ V (φ m)
hφB : (𝓤 X).HasAntitoneBasis (V ∘ φ)
⊢ ∃ U, (∀ (n : ℕ), SymmetricRel (U n)) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U

Proof state:
case neg
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
h : ¬∃ n, (x, y) ∉ U n
⊢ 0 = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i

Tactic:
simpa only [not_exists, Classical.not_not, eq_self_iff_true, true_iff] using h

Result:
no goals