awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
rw : ¬L.length ≤ m
⊢ m ≤ l.length

Tactic:
rw [← not_lt, Nat.lt_iff_add_one_le, ← hL_len]

Premises used: Nat.lt_iff_add_one_le, not_lt
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
hLm : L.length ≤ m
rw : ∀ (hm : List.IsChain (fun (x y : X) ↦ d x y = 0) (x :: l ++ [y])) (hLm : L.length ≤ m), False
rw₁ : ∀ (hm : Forall (fun (x : ℝ≥0) ↦ x = 0) L) (hLm : L.length ≤ m), (x :: l).length = (l ++ [y]).length
⊢ False

Tactic:
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,
          ← isChain_cons_append_singleton_iff_forall₂]
          at hm

Premises used: List.sum_eq_zero_iff, two_mul, List.take_of_length_le, List.isChain_cons_append_singleton_iff_forall₂, add_le_iff_nonpos_left, Set.mem_setOf_eq, List.forall_iff_forall_mem, List.forall_zipWith, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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 : Forall (fun (x : ℝ≥0) ↦ x = 0) L
hLm : L.length ≤ m
⊢ (x :: l).length = (l ++ [y]).length

Tactic:
simp
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
hLm : L.length ≤ m
⊢ List.IsChain (fun (x y : X) ↦ d x y = 0) (x :: l ++ [y])

Tactic:
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,
          ← isChain_cons_append_singleton_iff_forall₂]
          at hm <;>
        [skip; simp]

Premises used: List.sum_eq_zero_iff, two_mul, List.take_of_length_le, List.isChain_cons_append_singleton_iff_forall₂, add_le_iff_nonpos_left, Set.mem_setOf_eq, List.forall_iff_forall_mem, List.forall_zipWith, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
hLm : L.length ≤ m
hm₁ : List.IsChain (fun (x y : X) ↦ d x y = 0) (x :: l ++ [y])
⊢ L.length ≤ m

Tactic:
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,
          ← isChain_cons_append_singleton_iff_forall₂]
          at hm <;>
        [skip; simp]

Premises used: List.sum_eq_zero_iff, two_mul, List.take_of_length_le, List.isChain_cons_append_singleton_iff_forall₂, add_le_iff_nonpos_left, Set.mem_setOf_eq, List.forall_iff_forall_mem, List.forall_zipWith, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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 : List.IsChain (fun (x y : X) ↦ d x y = 0) (x :: l ++ [y])
hLm : L.length ≤ m
⊢ False

Tactic:
hd₀ (hm.rel_cons (mem_append.2 <| Or.inr <| mem_singleton_self _))

Premises used: Iff.mpr, List.IsChain.rel_cons, List.mem_singleton_self, List.mem_append, Or.inr
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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 : List.IsChain (fun (x y : X) ↦ d x y = 0) (x :: l ++ [y])
hLm : L.length ≤ m
⊢ False

Tactic:
exact hd₀ (hm.rel_cons (mem_append.2 <| Or.inr <| mem_singleton_self _))

Premises used: Iff.mpr, List.IsChain.rel_cons, List.mem_singleton_self, List.mem_append, Or.inr
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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:
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,
          ← isChain_cons_append_singleton_iff_forall₂]
          at hm <;>
        [skip; simp]
      exact hd₀ (hm.rel_cons (mem_append.2 <| Or.inr <| mem_singleton_self _))
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
hs_ub : l.length ∈ upperBounds s
⊢ BddAbove s

Tactic:
have hs_bdd : BddAbove s := ⟨length l, hs_ub⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
hs_ub : l.length ∈ upperBounds s
hs_bdd : BddAbove s
⊢ ∃ M ≤ l.length, IsGreatest s M

Tactic:
⟨sSup s, csSup_le hsne hs_ub, ⟨Nat.sSup_mem hsne hs_bdd, fun k => le_csSup hs_bdd⟩⟩

Premises used: Nat.sSup_mem, And.intro, Exists.intro, le_csSup, csSup_le, SupSet.sSup
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
hs_ub : l.length ∈ upperBounds s
hs_bdd : BddAbove s
⊢ ∃ M ≤ l.length, IsGreatest s M

Tactic:
exact ⟨sSup s, csSup_le hsne hs_ub, ⟨Nat.sSup_mem hsne hs_bdd, fun k => le_csSup hs_bdd⟩⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
obtain :
  ∀ (M : ℕ) (hMl : M ≤ l.length) (hMs : IsGreatest s M),
    ∃ (z : X) (z' : X), d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum
⊢ ∃ (z : X) (z' : X), 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,
          ← isChain_cons_append_singleton_iff_forall₂]
          at hm <;>
        [skip; simp]
      exact hd₀ (hm.rel_cons (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⟩⟩

Premises used: List.length
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
rwa : M < l.length + 1
rwa₁ rwa₂ rwa₃ rwa₄ : M ≤ l.length
⊢ M < L.length

Tactic:
rwa [hL_len, Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
⊢ M < L.length

Tactic:
have hM_lt : M < length L := by rwa [hL_len, Nat.lt_succ_iff]
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
hM_lt : M < L.length
⊢ M < (x :: l).length

Tactic:
have hM_ltx : M < length (x::l) := lt_length_left_of_zipWith hM_lt
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
⊢ M < (l ++ [y]).length

Tactic:
have hM_lty : M < length (l ++ [y]) := lt_length_right_of_zipWith hM_lt
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
⊢ ∃ (z : X) (z' : X), d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum

Tactic:
⟨(x::l)[M], (l ++ [y])[M], ?_, ?_, ?_⟩

Premises used: List.cons, GetElem.getElem, And.intro, Exists.intro, HAppend.hAppend, List.nil
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
refine_1 : d x (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (x :: l) M hM_ltx) ≤ L.sum
refine_2 :
  d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (x :: l) M hM_ltx)
      (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (l ++ [y]) M hM_lty) ≤
    L.sum
refine_3 : d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (l ++ [y]) M hM_lty) y ≤ L.sum
⊢ ∃ (z : X) (z' : X), d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum

Tactic:
refine ⟨(x::l)[M], (l ++ [y])[M], ?_, ?_, ?_⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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
hMl : 0 ≤ l.length
hMs : IsGreatest s 0
hM_lt : 0 < L.length
hM_ltx : 0 < (x :: l).length
hM_lty : 0 < (l ++ [y]).length
⊢ d x (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (x :: l) 0 hM_ltx) ≤ L.sum

Tactic:
simp [dist_self]
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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 + 1 ≤ l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
refine_1 :
  ∀ (hMl : M < l.length) (hMs : IsGreatest s (M + 1)) (hM_lt : M + 1 < L.length) (hM_ltx : M + 1 < (x :: l).length)
    (hM_lty : M + 1 < (l ++ [y]).length),
    d x (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (x :: l) (M + 1) hM_ltx) ≤ L.sum
⊢ d x (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (x :: l) (M + 1) hM_ltx) ≤ L.sum

Tactic:
rw [Nat.succ_le_iff] at hMl

Premises used: Nat.succ_le_iff
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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 + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
⊢ (take M l).length = M

Tactic:
have hMl' : length (take M l) = M := length_take.trans (min_eq_left hMl.le)
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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 + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
hMl' : (take M l).length = M
⊢ d x (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (x :: l) (M + 1) hM_ltx) ≤ L.sum

Tactic:
(ihn _ hMl _ _ _ hMl').trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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 + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
hMl' : (take M l).length = M
refine_1 :
  2 *
      (zipWith d (x :: take M l)
          (take M l ++ [getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (x :: l) (M + 1) hM_ltx])).sum ≤
    L.sum
⊢ d x (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (x :: l) (M + 1) hM_ltx) ≤ L.sum

Tactic:
refine (ihn _ hMl _ _ _ hMl').trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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 + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
hMl' : (take M l).length = M
⊢ 2 * (take (M + 1) L).sum ≤ L.sum

Tactic:
hMs.1.out

Premises used: Membership.mem.out, And.left
-- Module: Mathlib.Topology.Metrizable.Uniformity
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₄))
this : IsTrans X fun (x y : X) ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X) (hn : 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 + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
hMl' : (take M l).length = M
h :
  zipWith d (x :: take M l)
      (take M l ++ [getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (x :: l) (M + 1) hM_ltx]) =
    take (M + 1) L
⊢ 2 *
      (zipWith d (x :: take M l)
          (take M l ++ [getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (x :: l) (M + 1) hM_ltx])).sum ≤
    L.sum

Tactic:
convert! hMs.1.out

Premises used: Membership.mem.out, And.left