[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x : X
⊢ sum (zipWith d [x] ([] ++ [x])) = 0
[PROOFSTEP]
simp [dist_self]
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
⊢ ⨅ (l : List X), sum (zipWith d (x :: l) (l ++ [y])) = ⨅ (l : List X), sum (zipWith d (y :: l) (l ++ [x]))
[PROOFSTEP]
refine' reverse_surjective.iInf_congr _ fun l => _
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
l : List X
⊢ sum (zipWith d (y :: reverse l) (reverse l ++ [x])) = sum (zipWith d (x :: l) (l ++ [y]))
[PROOFSTEP]
rw [← sum_reverse, zipWith_distrib_reverse, reverse_append, reverse_reverse, reverse_singleton, singleton_append,
  reverse_cons, reverse_reverse, zipWith_comm_of_comm _ dist_comm]
[GOAL]
case h
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
l : List X
⊢ length (y :: reverse l) = length (reverse l ++ [x])
[PROOFSTEP]
simp only [length, length_append]
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
unfold dist
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
⊢ { dist := fun x y => ↑(⨅ (l : List X), sum (zipWith d (x :: l) (l ++ [y]))) }.1 x z ≤
    { dist := fun x y => ↑(⨅ (l : List X), sum (zipWith d (x :: l) (l ++ [y]))) }.1 x y +
      { dist := fun x y => ↑(⨅ (l : List X), sum (zipWith d (x :: l) (l ++ [y]))) }.1 y z
[PROOFSTEP]
rw [← NNReal.coe_add, NNReal.coe_le_coe]
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
⊢ ⨅ (l : List X), sum (zipWith d (x :: l) (l ++ [z])) ≤
    (⨅ (l : List X), sum (zipWith d (x :: l) (l ++ [y]))) + ⨅ (l : List X), sum (zipWith d (y :: l) (l ++ [z]))
[PROOFSTEP]
refine' NNReal.le_iInf_add_iInf fun lxy lyz => _
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ ⨅ (l : List X), sum (zipWith d (x :: l) (l ++ [z])) ≤
    sum (zipWith d (x :: lxy) (lxy ++ [y])) + sum (zipWith d (y :: lyz) (lyz ++ [z]))
[PROOFSTEP]
calc
  ⨅ l, (zipWith d (x :: l) (l ++ [z])).sum ≤ (zipWith d (x :: lxy ++ y :: lyz) ((lxy ++ y :: lyz) ++ [z])).sum :=
    ciInf_le (OrderBot.bddBelow _) (lxy ++ y :: lyz)
  _ = (zipWith d (x :: lxy) (lxy ++ [y])).sum + (zipWith d (y :: lyz) (lyz ++ [z])).sum :=
    by
    rw [← sum_append, ← zipWith_append, cons_append, ← @singleton_append _ y, append_assoc, append_assoc, append_assoc]
    rw [length_cons, length_append, length_singleton]
      -- Porting note: `edist_dist` is no longer inferred
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ sum (zipWith d (x :: lxy ++ y :: lyz) (lxy ++ y :: lyz ++ [z])) =
    sum (zipWith d (x :: lxy) (lxy ++ [y])) + sum (zipWith d (y :: lyz) (lyz ++ [z]))
[PROOFSTEP]
rw [← sum_append, ← zipWith_append, cons_append, ← @singleton_append _ y, append_assoc, append_assoc, append_assoc]
[GOAL]
case h
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ length (x :: lxy) = length (lxy ++ [y])
[PROOFSTEP]
rw [length_cons, length_append, length_singleton]
  -- Porting note: `edist_dist` is no longer inferred
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
⊢ sum (zipWith d [x] ([] ++ [y])) = d x y
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
⊢ ↑(d x y) ≤ 2 * dist x y
[PROOFSTEP]
rw [dist_ofPreNNDist, ← NNReal.coe_two, ← NNReal.coe_mul, NNReal.mul_iInf, NNReal.coe_le_coe]
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
⊢ d x y ≤ ⨅ (i : List X), 2 * sum (zipWith d (x :: i) (i ++ [y]))
[PROOFSTEP]
refine' le_ciInf fun l => _
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
⊢ d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
[PROOFSTEP]
have hd₀_trans : Transitive fun x y => d x y = 0 :=
  by
  intro a b c hab hbc
  rw [← nonpos_iff_eq_zero]
  simpa only [nonpos_iff_eq_zero, hab, hbc, dist_self c, max_self, mul_zero] using hd a b c c
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
⊢ Transitive fun x y => d x y = 0
[PROOFSTEP]
intro a b c hab hbc
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
a b c : X
hab : d a b = 0
hbc : d b c = 0
⊢ d a c = 0
[PROOFSTEP]
rw [← nonpos_iff_eq_zero]
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
a b c : X
hab : d a b = 0
hbc : d b c = 0
⊢ d a c ≤ 0
[PROOFSTEP]
simpa only [nonpos_iff_eq_zero, hab, hbc, dist_self c, max_self, mul_zero] using hd a b c c
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
hd₀_trans : Transitive fun x y => d x y = 0
⊢ d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
[PROOFSTEP]
haveI : IsTrans X fun x y => d x y = 0 := ⟨hd₀_trans⟩
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
⊢ d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
[PROOFSTEP]
induction' hn : length l using Nat.strong_induction_on with n ihn generalizing x y l
[GOAL]
case h
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn✝ : length l✝ = x✝
n : ℕ
ihn : ∀ (m : ℕ), m < n → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
x y : X
l : List X
hn : length l = n
⊢ d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
[PROOFSTEP]
simp only at ihn 
[GOAL]
case h
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn✝ : length l✝ = x✝
n : ℕ
ihn : ∀ (m : ℕ), m < n → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
x y : X
l : List X
hn : length l = n
⊢ d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
[PROOFSTEP]
subst n
[GOAL]
case h
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
⊢ d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
[PROOFSTEP]
set L := zipWith d (x :: l) (l ++ [y])
[GOAL]
case h
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
⊢ d x y ≤ 2 * sum L
[PROOFSTEP]
have hL_len : length L = length l + 1 := by simp
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
⊢ length L = length l + 1
[PROOFSTEP]
simp
[GOAL]
case h
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
⊢ d x y ≤ 2 * sum L
[PROOFSTEP]
cases' eq_or_ne (d x y) 0 with hd₀ hd₀
[GOAL]
case h.inl
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y = 0
⊢ d x y ≤ 2 * sum L
[PROOFSTEP]
simp only [hd₀, zero_le]
[GOAL]
case h.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
⊢ d x y ≤ 2 * sum L
[PROOFSTEP]
rsuffices ⟨z, z', hxz, hzz', hz'y⟩ : ∃ z z' : X, d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum
[GOAL]
case h.inr.intro.intro.intro.intro
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
z z' : X
hxz : d x z ≤ sum L
hzz' : d z z' ≤ sum L
hz'y : d z' y ≤ sum L
⊢ d x y ≤ 2 * sum L
[PROOFSTEP]
exact (hd x z z' y).trans (mul_le_mul_left' (max_le hxz (max_le hzz' hz'y)) _)
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
⊢ ∃ z z', d x z ≤ sum L ∧ d z z' ≤ sum L ∧ d z' y ≤ sum L
[PROOFSTEP]
set s : Set ℕ := {m : ℕ | 2 * (take m L).sum ≤ L.sum}
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
⊢ ∃ z z', d x z ≤ sum L ∧ d z z' ≤ sum L ∧ d z' y ≤ sum L
[PROOFSTEP]
have hs₀ : 0 ∈ s := by simp
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
⊢ 0 ∈ s
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
⊢ ∃ z z', d x z ≤ sum L ∧ d z z' ≤ sum L ∧ d z' y ≤ sum L
[PROOFSTEP]
have hsne : s.Nonempty := ⟨0, hs₀⟩
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
⊢ ∃ z z', d x z ≤ sum L ∧ d z z' ≤ sum L ∧ d z' y ≤ sum L
[PROOFSTEP]
obtain ⟨M, hMl, hMs⟩ : ∃ M ≤ length l, IsGreatest s M :=
  by
  have hs_ub : length l ∈ upperBounds s := by
    intro m hm
    rw [← not_lt, Nat.lt_iff_add_one_le, ← hL_len]
    intro hLm
    rw [mem_setOf_eq, take_all_of_le hLm, two_mul, add_le_iff_nonpos_left, nonpos_iff_eq_zero, sum_eq_zero_iff, ←
        all₂_iff_forall, all₂_zipWith, ← chain_append_singleton_iff_forall₂] at hm  <;>
      [skip; simp]
    exact hd₀ (hm.rel (mem_append.2 <| Or.inr <| mem_singleton_self _))
  have hs_bdd : BddAbove s := ⟨length l, hs_ub⟩
  exact ⟨sSup s, csSup_le hsne hs_ub, ⟨Nat.sSup_mem hsne hs_bdd, fun k => le_csSup hs_bdd⟩⟩
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
⊢ ∃ M, M ≤ length l ∧ IsGreatest s M
[PROOFSTEP]
have hs_ub : length l ∈ upperBounds s := by
  intro m hm
  rw [← not_lt, Nat.lt_iff_add_one_le, ← hL_len]
  intro hLm
  rw [mem_setOf_eq, take_all_of_le hLm, two_mul, add_le_iff_nonpos_left, nonpos_iff_eq_zero, sum_eq_zero_iff, ←
      all₂_iff_forall, all₂_zipWith, ← chain_append_singleton_iff_forall₂] at hm  <;>
    [skip; simp]
  exact hd₀ (hm.rel (mem_append.2 <| Or.inr <| mem_singleton_self _))
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
⊢ length l ∈ upperBounds s
[PROOFSTEP]
intro m hm
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
m : ℕ
hm : m ∈ s
⊢ m ≤ length l
[PROOFSTEP]
rw [← not_lt, Nat.lt_iff_add_one_le, ← hL_len]
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
m : ℕ
hm : m ∈ s
⊢ ¬length L ≤ m
[PROOFSTEP]
intro hLm
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
m : ℕ
hm : m ∈ s
hLm : length L ≤ m
⊢ False
[PROOFSTEP]
rw [mem_setOf_eq, take_all_of_le hLm, two_mul, add_le_iff_nonpos_left, nonpos_iff_eq_zero, sum_eq_zero_iff, ←
    all₂_iff_forall, all₂_zipWith, ← chain_append_singleton_iff_forall₂] at hm  <;>
  [skip; simp]
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
m : ℕ
hm : m ∈ s
hLm : length L ≤ m
⊢ False
[PROOFSTEP]
rw [mem_setOf_eq, take_all_of_le hLm, two_mul, add_le_iff_nonpos_left, nonpos_iff_eq_zero, sum_eq_zero_iff, ←
  all₂_iff_forall, all₂_zipWith, ← chain_append_singleton_iff_forall₂] at hm 
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
m : ℕ
hm : Chain (fun x y => d x y = 0) x (l ++ [y])
hLm : length L ≤ m
⊢ False
[PROOFSTEP]
skip
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
m : ℕ
hm : All₂ (fun x => x = 0) L
hLm : length L ≤ m
⊢ length (x :: l) = length (l ++ [y])
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
m : ℕ
hm : Chain (fun x y => d x y = 0) x (l ++ [y])
hLm : length L ≤ m
⊢ False
[PROOFSTEP]
exact hd₀ (hm.rel (mem_append.2 <| Or.inr <| mem_singleton_self _))
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
hs_ub : length l ∈ upperBounds s
⊢ ∃ M, M ≤ length l ∧ IsGreatest s M
[PROOFSTEP]
have hs_bdd : BddAbove s := ⟨length l, hs_ub⟩
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
hs_ub : length l ∈ upperBounds s
hs_bdd : BddAbove s
⊢ ∃ M, M ≤ length l ∧ IsGreatest s M
[PROOFSTEP]
exact ⟨sSup s, csSup_le hsne hs_ub, ⟨Nat.sSup_mem hsne hs_bdd, fun k => le_csSup hs_bdd⟩⟩
[GOAL]
case intro.intro
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M ≤ length l
hMs : IsGreatest s M
⊢ ∃ z z', d x z ≤ sum L ∧ d z z' ≤ sum L ∧ d z' y ≤ sum L
[PROOFSTEP]
have hM_lt : M < length L := by rwa [hL_len, Nat.lt_succ_iff]
[GOAL]
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M ≤ length l
hMs : IsGreatest s M
⊢ M < length L
[PROOFSTEP]
rwa [hL_len, Nat.lt_succ_iff]
[GOAL]
case intro.intro
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
⊢ ∃ z z', d x z ≤ sum L ∧ d z z' ≤ sum L ∧ d z' y ≤ sum L
[PROOFSTEP]
have hM_ltx : M < length (x :: l) := lt_length_left_of_zipWith hM_lt
[GOAL]
case intro.intro
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
⊢ ∃ z z', d x z ≤ sum L ∧ d z z' ≤ sum L ∧ d z' y ≤ sum L
[PROOFSTEP]
have hM_lty : M < length (l ++ [y]) := lt_length_right_of_zipWith hM_lt
[GOAL]
case intro.intro
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
⊢ ∃ z z', d x z ≤ sum L ∧ d z z' ≤ sum L ∧ d z' y ≤ sum L
[PROOFSTEP]
refine' ⟨(x :: l).get ⟨M, hM_ltx⟩, (l ++ [y]).get ⟨M, hM_lty⟩, _, _, _⟩
[GOAL]
case intro.intro.refine'_1
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
⊢ d x (List.get (x :: l) { val := M, isLt := hM_ltx }) ≤ sum L
[PROOFSTEP]
cases M with
| zero => simp [dist_self, List.get]
| succ M =>
  rw [Nat.succ_le_iff] at hMl 
  have hMl' : length (take M l) = M := (length_take _ _).trans (min_eq_left hMl.le)
  simp only [List.get]
  refine' (ihn _ hMl _ _ _ hMl').trans _
  convert hMs.1.out
  rw [zipWith_distrib_take, take, take_succ, get?_append hMl, get?_eq_get hMl, ← Option.coe_def, Option.to_list_some,
    take_append_of_le_length hMl.le]
[GOAL]
case intro.intro.refine'_1
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
⊢ d x (List.get (x :: l) { val := M, isLt := hM_ltx }) ≤ sum L
[PROOFSTEP]
cases M with
| zero => simp [dist_self, List.get]
| succ M =>
  rw [Nat.succ_le_iff] at hMl 
  have hMl' : length (take M l) = M := (length_take _ _).trans (min_eq_left hMl.le)
  simp only [List.get]
  refine' (ihn _ hMl _ _ _ hMl').trans _
  convert hMs.1.out
  rw [zipWith_distrib_take, take, take_succ, get?_append hMl, get?_eq_get hMl, ← Option.coe_def, Option.to_list_some,
    take_append_of_le_length hMl.le]
[GOAL]
case intro.intro.refine'_1.zero
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
hMl : Nat.zero ≤ length l
hMs : IsGreatest s Nat.zero
hM_lt : Nat.zero < length L
hM_ltx : Nat.zero < length (x :: l)
hM_lty : Nat.zero < length (l ++ [y])
⊢ d x (List.get (x :: l) { val := Nat.zero, isLt := hM_ltx }) ≤ sum L
[PROOFSTEP]

| zero => simp [dist_self, List.get]
[GOAL]
case intro.intro.refine'_1.zero
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
hMl : Nat.zero ≤ length l
hMs : IsGreatest s Nat.zero
hM_lt : Nat.zero < length L
hM_ltx : Nat.zero < length (x :: l)
hM_lty : Nat.zero < length (l ++ [y])
⊢ d x (List.get (x :: l) { val := Nat.zero, isLt := hM_ltx }) ≤ sum L
[PROOFSTEP]
simp [dist_self, List.get]
[GOAL]
case intro.intro.refine'_1.succ
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : Nat.succ M ≤ length l
hMs : IsGreatest s (Nat.succ M)
hM_lt : Nat.succ M < length L
hM_ltx : Nat.succ M < length (x :: l)
hM_lty : Nat.succ M < length (l ++ [y])
⊢ d x (List.get (x :: l) { val := Nat.succ M, isLt := hM_ltx }) ≤ sum L
[PROOFSTEP]

| succ M =>
  rw [Nat.succ_le_iff] at hMl 
  have hMl' : length (take M l) = M := (length_take _ _).trans (min_eq_left hMl.le)
  simp only [List.get]
  refine' (ihn _ hMl _ _ _ hMl').trans _
  convert hMs.1.out
  rw [zipWith_distrib_take, take, take_succ, get?_append hMl, get?_eq_get hMl, ← Option.coe_def, Option.to_list_some,
    take_append_of_le_length hMl.le]
[GOAL]
case intro.intro.refine'_1.succ
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : Nat.succ M ≤ length l
hMs : IsGreatest s (Nat.succ M)
hM_lt : Nat.succ M < length L
hM_ltx : Nat.succ M < length (x :: l)
hM_lty : Nat.succ M < length (l ++ [y])
⊢ d x (List.get (x :: l) { val := Nat.succ M, isLt := hM_ltx }) ≤ sum L
[PROOFSTEP]
rw [Nat.succ_le_iff] at hMl 
[GOAL]
case intro.intro.refine'_1.succ
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M < length l
hMs : IsGreatest s (Nat.succ M)
hM_lt : Nat.succ M < length L
hM_ltx : Nat.succ M < length (x :: l)
hM_lty : Nat.succ M < length (l ++ [y])
⊢ d x (List.get (x :: l) { val := Nat.succ M, isLt := hM_ltx }) ≤ sum L
[PROOFSTEP]
have hMl' : length (take M l) = M := (length_take _ _).trans (min_eq_left hMl.le)
[GOAL]
case intro.intro.refine'_1.succ
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M < length l
hMs : IsGreatest s (Nat.succ M)
hM_lt : Nat.succ M < length L
hM_ltx : Nat.succ M < length (x :: l)
hM_lty : Nat.succ M < length (l ++ [y])
hMl' : length (take M l) = M
⊢ d x (List.get (x :: l) { val := Nat.succ M, isLt := hM_ltx }) ≤ sum L
[PROOFSTEP]
simp only [List.get]
[GOAL]
case intro.intro.refine'_1.succ
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M < length l
hMs : IsGreatest s (Nat.succ M)
hM_lt : Nat.succ M < length L
hM_ltx : Nat.succ M < length (x :: l)
hM_lty : Nat.succ M < length (l ++ [y])
hMl' : length (take M l) = M
⊢ d x (List.get l { val := M, isLt := (_ : Nat.succ M ≤ length l) }) ≤ sum (zipWith d (x :: l) (l ++ [y]))
[PROOFSTEP]
refine' (ihn _ hMl _ _ _ hMl').trans _
[GOAL]
case intro.intro.refine'_1.succ
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M < length l
hMs : IsGreatest s (Nat.succ M)
hM_lt : Nat.succ M < length L
hM_ltx : Nat.succ M < length (x :: l)
hM_lty : Nat.succ M < length (l ++ [y])
hMl' : length (take M l) = M
⊢ 2 * sum (zipWith d (x :: take M l) (take M l ++ [List.get l { val := M, isLt := (_ : Nat.succ M ≤ length l) }])) ≤
    sum (zipWith d (x :: l) (l ++ [y]))
[PROOFSTEP]
convert hMs.1.out
[GOAL]
case h.e'_3.h.e'_6.h.e'_4
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M < length l
hMs : IsGreatest s (Nat.succ M)
hM_lt : Nat.succ M < length L
hM_ltx : Nat.succ M < length (x :: l)
hM_lty : Nat.succ M < length (l ++ [y])
hMl' : length (take M l) = M
⊢ zipWith d (x :: take M l) (take M l ++ [List.get l { val := M, isLt := (_ : Nat.succ M ≤ length l) }]) =
    take (Nat.succ M) L
[PROOFSTEP]
rw [zipWith_distrib_take, take, take_succ, get?_append hMl, get?_eq_get hMl, ← Option.coe_def, Option.to_list_some,
  take_append_of_le_length hMl.le]
[GOAL]
case intro.intro.refine'_2
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
⊢ d (List.get (x :: l) { val := M, isLt := hM_ltx }) (List.get (l ++ [y]) { val := M, isLt := hM_lty }) ≤ sum L
[PROOFSTEP]
exact single_le_sum (fun x _ => zero_le x) _ (mem_iff_get.2 ⟨⟨M, hM_lt⟩, get_zipWith⟩)
[GOAL]
case intro.intro.refine'_3
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
⊢ d (List.get (l ++ [y]) { val := M, isLt := hM_lty }) y ≤ sum L
[PROOFSTEP]
rcases hMl.eq_or_lt with (rfl | hMl)
[GOAL]
case intro.intro.refine'_3.inl
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
hMl : length l ≤ length l
hMs : IsGreatest s (length l)
hM_lt : length l < length L
hM_ltx : length l < length (x :: l)
hM_lty : length l < length (l ++ [y])
⊢ d (List.get (l ++ [y]) { val := length l, isLt := hM_lty }) y ≤ sum L
[PROOFSTEP]
simp only [get_append_right' le_rfl, sub_self, get_singleton, dist_self, zero_le]
[GOAL]
case intro.intro.refine'_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl✝ : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
hMl : M < length l
⊢ d (List.get (l ++ [y]) { val := M, isLt := hM_lty }) y ≤ sum L
[PROOFSTEP]
rw [get_append _ hMl]
[GOAL]
case intro.intro.refine'_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl✝ : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
hMl : M < length l
⊢ d (List.get l { val := M, isLt := hMl }) y ≤ sum L
[PROOFSTEP]
have hlen : length (drop (M + 1) l) = length l - (M + 1) := length_drop _ _
[GOAL]
case intro.intro.refine'_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl✝ : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
hMl : M < length l
hlen : length (drop (M + 1) l) = length l - (M + 1)
⊢ d (List.get l { val := M, isLt := hMl }) y ≤ sum L
[PROOFSTEP]
have hlen_lt : length l - (M + 1) < length l := Nat.sub_lt_of_pos_le M.succ_pos hMl
[GOAL]
case intro.intro.refine'_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl✝ : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
hMl : M < length l
hlen : length (drop (M + 1) l) = length l - (M + 1)
hlen_lt : length l - (M + 1) < length l
⊢ d (List.get l { val := M, isLt := hMl }) y ≤ sum L
[PROOFSTEP]
refine' (ihn _ hlen_lt _ y _ hlen).trans _
[GOAL]
case intro.intro.refine'_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl✝ : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
hMl : M < length l
hlen : length (drop (M + 1) l) = length l - (M + 1)
hlen_lt : length l - (M + 1) < length l
⊢ 2 * sum (zipWith d (List.get l { val := M, isLt := hMl } :: drop (M + 1) l) (drop (M + 1) l ++ [y])) ≤ sum L
[PROOFSTEP]
rw [cons_get_drop_succ]
[GOAL]
case intro.intro.refine'_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl✝ : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
hMl : M < length l
hlen : length (drop (M + 1) l) = length l - (M + 1)
hlen_lt : length l - (M + 1) < length l
⊢ 2 * sum (zipWith d (drop (↑{ val := M, isLt := hMl }) l) (drop (M + 1) l ++ [y])) ≤ sum L
[PROOFSTEP]
have hMs' : L.sum ≤ 2 * (L.take (M + 1)).sum := not_lt.1 fun h => (hMs.2 h.le).not_lt M.lt_succ_self
[GOAL]
case intro.intro.refine'_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl✝ : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
hMl : M < length l
hlen : length (drop (M + 1) l) = length l - (M + 1)
hlen_lt : length l - (M + 1) < length l
hMs' : sum L ≤ 2 * sum (take (M + 1) L)
⊢ 2 * sum (zipWith d (drop (↑{ val := M, isLt := hMl }) l) (drop (M + 1) l ++ [y])) ≤ sum L
[PROOFSTEP]
rw [← sum_take_add_sum_drop L (M + 1), two_mul, add_le_add_iff_left, ← add_le_add_iff_right, sum_take_add_sum_drop, ←
  two_mul] at hMs' 
[GOAL]
case intro.intro.refine'_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl✝ : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
hMl : M < length l
hlen : length (drop (M + 1) l) = length l - (M + 1)
hlen_lt : length l - (M + 1) < length l
hMs'✝ : sum (drop (M + 1) L) ≤ sum (take (M + 1) L)
hMs' : 2 * sum (drop (M + 1) L) ≤ sum L
⊢ 2 * sum (zipWith d (drop (↑{ val := M, isLt := hMl }) l) (drop (M + 1) l ++ [y])) ≤ sum L
[PROOFSTEP]
convert hMs'
[GOAL]
case h.e'_3.h.e'_6.h.e'_4
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x✝¹ y✝ : X
l✝ : List X
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x✝ : ℕ
hn : length l✝ = x✝
x y : X
l : List X
ihn : ∀ (m : ℕ), m < length l → ∀ (x y : X) (l : List X), length l = m → d x y ≤ 2 * sum (zipWith d (x :: l) (l ++ [y]))
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : length L = length l + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * sum (take m L) ≤ sum L}
hs₀ : 0 ∈ s
hsne : Set.Nonempty s
M : ℕ
hMl✝ : M ≤ length l
hMs : IsGreatest s M
hM_lt : M < length L
hM_ltx : M < length (x :: l)
hM_lty : M < length (l ++ [y])
hMl : M < length l
hlen : length (drop (M + 1) l) = length l - (M + 1)
hlen_lt : length l - (M + 1) < length l
hMs'✝ : sum (drop (M + 1) L) ≤ sum (take (M + 1) L)
hMs' : 2 * sum (drop (M + 1) L) ≤ sum L
⊢ zipWith d (drop (↑{ val := M, isLt := hMl }) l) (drop (M + 1) l ++ [y]) = drop (M + 1) L
[PROOFSTEP]
rwa [zipWith_distrib_drop, drop, drop_append_of_le_length]
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
[PROOFSTEP]
classical
  /- Choose a fast decreasing antitone basis `U : ℕ → set (X × X)` of the uniformity filter `𝓤 X`.
      Define `d x y : ℝ≥0` to be `(1 / 2) ^ n`, where `n` is the minimal index of `U n` that
      separates `x` and `y`: `(x, y) ∉ U n`, or `0` if `x` is not separated from `y`. This function
      satisfies the assumptions of `PseudoMetricSpace.ofPreNNDist` and
      `PseudoMetricSpace.le_two_mul_dist_ofPreNNDist`, hence the distance given by the former pseudo
      metric space structure is Lipschitz equivalent to the `d`. Thus the uniformities generated by
      `d` and `dist` are equal. Since the former uniformity is equal to `𝓤 X`, the latter is equal to
      `𝓤 X` as well. -/
obtain ⟨U, hU_symm, hU_comp, hB⟩ :
  ∃ U : ℕ → Set (X × X),
    (∀ n, SymmetricRel (U n)) ∧ (∀ ⦃m n⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U :=
  by
  rcases UniformSpace.has_seq_basis X with ⟨V, hB, hV_symm⟩
  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⟩
  exact ⟨V ∘ φ, fun n => hV_symm _, hφ_comp, hφB⟩
letI := UniformSpace.separationSetoid X
set d : X → X → ℝ≥0 := fun x y => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
have hd₀ : ∀ {x y}, d x y = 0 ↔ x ≈ y := by
  intro x y
  refine' Iff.trans _ hB.mem_separationRel.symm
  simp only [true_imp_iff]
  split_ifs with h
  · rw [← not_forall] at h 
    simp [h, pow_eq_zero_iff']
  · simpa only [not_exists, Classical.not_not, eq_self_iff_true, true_iff_iff] using h
have hd_symm : ∀ x y, d x y = d y x := by
  intro x y
  simp only [@SymmetricRel.mk_mem_comm _ _ (hU_symm _) x y]
have hr : (1 / 2 : ℝ≥0) ∈ Ioo (0 : ℝ≥0) 1 := ⟨half_pos one_pos, NNReal.half_lt_self one_ne_zero⟩
letI I := PseudoMetricSpace.ofPreNNDist d (fun x => hd₀.2 (Setoid.refl _)) hd_symm
have hdist_le : ∀ x y, dist x y ≤ d x y := PseudoMetricSpace.dist_ofPreNNDist_le _ _ _
have hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n :=
  by
  intro x y n
  dsimp only []
  split_ifs with h
  · rw [(strictAnti_pow hr.1 hr.2).le_iff_le, Nat.find_le_iff]
    exact ⟨fun ⟨m, hmn, hm⟩ hn => hm (hB.antitone hmn hn), fun h => ⟨n, le_rfl, h⟩⟩
  · push_neg at h 
    simp only [h, not_true, (pow_pos hr.1 _).not_le]
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 [← NNReal.div_le_iff' two_ne_zero, ← 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 _)
          -- Porting note: without the next line, `uniformity_basis_dist_pow` ends up introducing some
            -- `Subtype.val` applications instead of `NNReal.toReal`.
rw [mem_Ioo, ← NNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hr 
refine' ⟨I, uniformSpace_eq <| (uniformity_basis_dist_pow hr.1 hr.2).ext hB.toHasBasis _ _⟩
· refine' fun n hn => ⟨n, hn, fun x hx => (hdist_le _ _).trans_lt _⟩
  rwa [← NNReal.coe_pow, NNReal.coe_lt_coe, ← not_le, hle_d, Classical.not_not, Prod.mk.eta]
· refine' fun n _ => ⟨n + 1, trivial, fun x hx => _⟩
  rw [mem_setOf_eq] at hx 
  contrapose! hx
  refine' le_trans _ ((div_le_iff' (zero_lt_two' ℝ)).2 (hd_le x.1 x.2))
  rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ', mul_one_div,
    NNReal.div_le_iff two_ne_zero, div_mul_cancel _ (two_ne_zero' ℝ≥0), hle_d, Prod.mk.eta]
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
[PROOFSTEP]
obtain ⟨U, hU_symm, hU_comp, hB⟩ :
  ∃ U : ℕ → Set (X × X),
    (∀ n, SymmetricRel (U n)) ∧ (∀ ⦃m n⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U :=
  by
  rcases UniformSpace.has_seq_basis X with ⟨V, hB, hV_symm⟩
  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⟩
  exact ⟨V ∘ φ, fun n => hV_symm _, hφ_comp, hφB⟩
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
⊢ ∃ U, (∀ (n : ℕ), SymmetricRel (U n)) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ HasAntitoneBasis (𝓤 X) U
[PROOFSTEP]
rcases UniformSpace.has_seq_basis X with ⟨V, hB, hV_symm⟩
[GOAL]
case intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
V : ℕ → Set (X × X)
hB : HasAntitoneBasis (𝓤 X) V
hV_symm : ∀ (n : ℕ), SymmetricRel (V n)
⊢ ∃ U, (∀ (n : ℕ), SymmetricRel (U n)) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ HasAntitoneBasis (𝓤 X) U
[PROOFSTEP]
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⟩
[GOAL]
case intro.intro.intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
V : ℕ → Set (X × X)
hB : HasAntitoneBasis (𝓤 X) 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 : HasAntitoneBasis (𝓤 X) (V ∘ φ)
⊢ ∃ U, (∀ (n : ℕ), SymmetricRel (U n)) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ HasAntitoneBasis (𝓤 X) U
[PROOFSTEP]
exact ⟨V ∘ φ, fun n => hV_symm _, hφ_comp, hφB⟩
[GOAL]
case intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
[PROOFSTEP]
letI := UniformSpace.separationSetoid X
[GOAL]
case intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
[PROOFSTEP]
set d : X → X → ℝ≥0 := fun x y => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
[GOAL]
case intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
d : X → X → ℝ≥0 := fun x y => if h : ∃ n, ¬(x, y) ∈ U n then (1 / 2) ^ Nat.find h else 0
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
[PROOFSTEP]
have hd₀ : ∀ {x y}, d x y = 0 ↔ x ≈ y := by
  intro x y
  refine' Iff.trans _ hB.mem_separationRel.symm
  simp only [true_imp_iff]
  split_ifs with h
  · rw [← not_forall] at h 
    simp [h, pow_eq_zero_iff']
  · simpa only [not_exists, Classical.not_not, eq_self_iff_true, true_iff_iff] using h
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ x ≈ y
[PROOFSTEP]
intro x y
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ x ≈ y
[PROOFSTEP]
refine' Iff.trans _ hB.mem_separationRel.symm
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ ∀ (i : ℕ), True → (x, y) ∈ U i
[PROOFSTEP]
simp only [true_imp_iff]
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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
⊢ (if h : ∃ n, ¬(x, y) ∈ U n then (1 / 2) ^ Nat.find h else 0) = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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
⊢ (1 / 2) ^ Nat.find h = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i
[PROOFSTEP]
rw [← not_forall] at h 
[GOAL]
case pos
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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
h : ¬∀ (x_1 : ℕ), (x, y) ∈ U x_1
⊢ (1 / 2) ^ Nat.find h✝ = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i
[PROOFSTEP]
simp [h, pow_eq_zero_iff']
[GOAL]
case neg
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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
[PROOFSTEP]
simpa only [not_exists, Classical.not_not, eq_self_iff_true, true_iff_iff] using h
[GOAL]
case intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ x ≈ y
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
[PROOFSTEP]
have hd_symm : ∀ x y, d x y = d y x := by
  intro x y
  simp only [@SymmetricRel.mk_mem_comm _ _ (hU_symm _) x y]
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ x ≈ y
⊢ ∀ (x y : X), d x y = d y x
[PROOFSTEP]
intro x y
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ x ≈ y
x y : X
⊢ d x y = d y x
[PROOFSTEP]
simp only [@SymmetricRel.mk_mem_comm _ _ (hU_symm _) x y]
[GOAL]
case intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ x ≈ y
hd_symm : ∀ (x y : X), d x y = d y x
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
[PROOFSTEP]
have hr : (1 / 2 : ℝ≥0) ∈ Ioo (0 : ℝ≥0) 1 := ⟨half_pos one_pos, NNReal.half_lt_self one_ne_zero⟩
[GOAL]
case intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ x ≈ y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
[PROOFSTEP]
letI I := PseudoMetricSpace.ofPreNNDist d (fun x => hd₀.2 (Setoid.refl _)) hd_symm
[GOAL]
case intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) hd_symm
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
[PROOFSTEP]
have hdist_le : ∀ x y, dist x y ≤ d x y := PseudoMetricSpace.dist_ofPreNNDist_le _ _ _
[GOAL]
case intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
[PROOFSTEP]
have hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n :=
  by
  intro x y n
  dsimp only []
  split_ifs with h
  · rw [(strictAnti_pow hr.1 hr.2).le_iff_le, Nat.find_le_iff]
    exact ⟨fun ⟨m, hmn, hm⟩ hn => hm (hB.antitone hmn hn), fun h => ⟨n, le_rfl, h⟩⟩
  · push_neg at h 
    simp only [h, not_true, (pow_pos hr.1 _).not_le]
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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
[PROOFSTEP]
intro x y n
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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
[PROOFSTEP]
dsimp only []
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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 h ↔ ¬(x, y) ∈ U n
[PROOFSTEP]
rw [(strictAnti_pow hr.1 hr.2).le_iff_le, Nat.find_le_iff]
[GOAL]
case pos
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x y : X
n : ℕ
h : ∃ n, ¬(x, y) ∈ U n
⊢ (∃ m, m ≤ n ∧ ¬(x, y) ∈ U m) ↔ ¬(x, y) ∈ U n
[PROOFSTEP]
exact ⟨fun ⟨m, hmn, hm⟩ hn => hm (hB.antitone hmn hn), fun h => ⟨n, le_rfl, h⟩⟩
[GOAL]
case neg
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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
[PROOFSTEP]
simp only [h, not_true, (pow_pos hr.1 _).not_le]
[GOAL]
case intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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.toUniformSpace = inst✝¹
[PROOFSTEP]
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 [← NNReal.div_le_iff' two_ne_zero, ← 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 _)
          -- Porting note: without the next line, `uniformity_basis_dist_pow` ends up introducing some
            -- `Subtype.val` applications instead of `NNReal.toReal`.
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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
[PROOFSTEP]
refine' PseudoMetricSpace.le_two_mul_dist_ofPreNNDist _ _ _ fun x₁ x₂ x₃ x₄ => _
[GOAL]
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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₄))
[PROOFSTEP]
by_cases H : ∃ n, (x₁, x₄) ∉ U n
[GOAL]
case pos
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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₄))
[PROOFSTEP]
refine' (dif_pos H).trans_le _
[GOAL]
case pos
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
[PROOFSTEP]
rw [← NNReal.div_le_iff' two_ne_zero, ← mul_one_div (_ ^ _), ← pow_succ']
[GOAL]
case pos
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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) ≤ max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
[PROOFSTEP]
simp only [le_max_iff, hle_d, ← not_and_or]
[GOAL]
case pos
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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))
[PROOFSTEP]
rintro ⟨h₁₂, h₂₃, h₃₄⟩
[GOAL]
case pos.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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
[PROOFSTEP]
refine' Nat.find_spec H (hU_comp (lt_add_one <| Nat.find H) _)
[GOAL]
case pos.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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)
⊢ (x₁, x₄) ∈ U (Nat.find H + 1) ○ (U (Nat.find H + 1) ○ U (Nat.find H + 1))
[PROOFSTEP]
exact ⟨x₂, h₁₂, x₃, h₂₃, h₃₄⟩
[GOAL]
case neg
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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₄))
[PROOFSTEP]
exact
  (dif_neg H).trans_le
    (zero_le _)
      -- Porting note: without the next line, `uniformity_basis_dist_pow` ends up introducing some
        -- `Subtype.val` applications instead of `NNReal.toReal`.
[GOAL]
case intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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✝¹
[PROOFSTEP]
rw [mem_Ioo, ← NNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hr 
[GOAL]
case intro.intro.intro
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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✝¹
[PROOFSTEP]
refine' ⟨I, uniformSpace_eq <| (uniformity_basis_dist_pow hr.1 hr.2).ext hB.toHasBasis _ _⟩
[GOAL]
case intro.intro.intro.refine'_1
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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 | dist p.fst p.snd < ↑(1 / 2) ^ i}
[PROOFSTEP]
refine' fun n hn => ⟨n, hn, fun x hx => (hdist_le _ _).trans_lt _⟩
[GOAL]
case intro.intro.intro.refine'_1
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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.fst x.snd) < ↑(1 / 2) ^ n
[PROOFSTEP]
rwa [← NNReal.coe_pow, NNReal.coe_lt_coe, ← not_le, hle_d, Classical.not_not, Prod.mk.eta]
[GOAL]
case intro.intro.intro.refine'_2
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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 | dist p.fst p.snd < ↑(1 / 2) ^ i} ⊆ U i'
[PROOFSTEP]
refine' fun n _ => ⟨n + 1, trivial, fun x hx => _⟩
[GOAL]
case intro.intro.intro.refine'_2
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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 ∈ {p | dist p.fst p.snd < ↑(1 / 2) ^ (n + 1)}
⊢ x ∈ U n
[PROOFSTEP]
rw [mem_setOf_eq] at hx 
[GOAL]
case intro.intro.intro.refine'_2
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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 : dist x.fst x.snd < ↑(1 / 2) ^ (n + 1)
⊢ x ∈ U n
[PROOFSTEP]
contrapose! hx
[GOAL]
case intro.intro.intro.refine'_2
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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.fst x.snd
[PROOFSTEP]
refine' le_trans _ ((div_le_iff' (zero_lt_two' ℝ)).2 (hd_le x.1 x.2))
[GOAL]
case intro.intro.intro.refine'_2
X✝ : Type u_1
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
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 : HasAntitoneBasis (𝓤 X) U
this : Setoid X := separationSetoid X
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 ↔ 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 (_ : ∀ (x : X), d x x = 0) 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.fst x.snd) / 2
[PROOFSTEP]
rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ', mul_one_div,
  NNReal.div_le_iff two_ne_zero, div_mul_cancel _ (two_ne_zero' ℝ≥0), hle_d, Prod.mk.eta]
[GOAL]
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
⊢ TopologicalSpace.PseudoMetrizableSpace X
[PROOFSTEP]
letI := UniformSpace.pseudoMetricSpace X
[GOAL]
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsCountablyGenerated (𝓤 X)
this : PseudoMetricSpace X := UniformSpace.pseudoMetricSpace X
⊢ TopologicalSpace.PseudoMetrizableSpace X
[PROOFSTEP]
infer_instance
[GOAL]
X : Type u_1
inst✝² : UniformSpace X
inst✝¹ : IsCountablyGenerated (𝓤 X)
inst✝ : T0Space X
⊢ TopologicalSpace.MetrizableSpace X
[PROOFSTEP]
letI := UniformSpace.metricSpace X
[GOAL]
X : Type u_1
inst✝² : UniformSpace X
inst✝¹ : IsCountablyGenerated (𝓤 X)
inst✝ : T0Space X
this : MetricSpace X := UniformSpace.metricSpace X
⊢ TopologicalSpace.MetrizableSpace X
[PROOFSTEP]
infer_instance
