-- Mathlib/Topology/Metrizable/Uniformity.lean
theorem le_two_mul_dist_ofPreNNDist (d : X → X → ℝ≥0) (dist_self : ∀ x, d x x = 0)
    (dist_comm : ∀ x y, d x y = d y x)
    (hd : ∀ 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
      (@PseudoMetricSpace.toDist X (PseudoMetricSpace.ofPreNNDist d dist_self dist_comm)) x y

Proof state:
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 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))
x y : X
l : List X
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
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

Result:
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 * (d x₁ x₂ ⊔ (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 * (zipWith d (x :: l) (l ++ [y])).sum

Proof state:
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 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
⊢ ∃ z z', d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum

Tactic:
set s : Set ℕ := { m : ℕ | 2 * (take m L).sum ≤ L.sum }

Result:
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 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
⊢ ∃ z z', d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum

Proof state:
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 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
set L := zipWith d (x::l) (l ++ [y])

Result:
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 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
⊢ d x y ≤ 2 * L.sum

Proof state:
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 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
⊢ ∃ z z', d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum

Tactic:
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_of_length_le hLm, two_mul, add_le_iff_nonpos_left, nonpos_iff_eq_zero,
        sum_eq_zero_iff, ← forall_iff_forall_mem, forall_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⟩⟩

Result:
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 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M ≤ l.length
hMs : IsGreatest s M
⊢ ∃ z z', d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum

Proof state:
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 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
⊢ l.length ∈ upperBounds s

Tactic:
intro m hm

Result:
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 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))
hd₀_trans : Transitive fun x y => d x y = 0
this : IsTrans X fun x y => d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
m : ℕ
hm : m ∈ s
⊢ m ≤ l.length