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 : ℕ
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 :
  ∀ (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
refine_1₁ :
  ∀ (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),
    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 hM_ltx) ≤ L.sum

Tactic:
cases M with
    | zero =>
      simp [dist_self]
    | succ M =>
      rw [Nat.succ_le_iff] at hMl
      have hMl' : length (take M l) = M := length_take.trans (min_eq_left hMl.le)
      refine (ihn _ hMl _ _ _ hMl').trans ?_
      convert! hMs.1.out
      rw [take_zipWith, take, take_add_one, getElem?_append_left hMl, getElem?_eq_getElem hMl,
        ← Option.coe_def, Option.toList_some, take_append_of_le_length hMl.le, getElem_cons_succ]

Premises used: Membership.mem.out, List.take_zipWith, List.getElem?_append_left, Option.coe_def, List.getElem?_eq_getElem, And.left, Option.toList_some, List.take_add_one, Nat.succ_le_iff, List.take, List.getElem_cons_succ
-- 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
⊢ 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

Tactic:
single_le_sum (fun x _ => zero_le) _ (mem_iff_get.2 ⟨⟨M, hM_lt⟩, getElem_zipWith⟩)

Premises used: Iff.mpr, zero_le, List.mem_iff_get, Fin.mk, List.single_le_sum, Exists.intro, List.getElem_zipWith
-- 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
⊢ 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

Tactic:
exact single_le_sum (fun x _ => zero_le) _ (mem_iff_get.2 ⟨⟨M, hM_lt⟩, getElem_zipWith⟩)

Premises used: Iff.mpr, zero_le, List.mem_iff_get, Fin.mk, List.single_le_sum, Exists.intro, List.getElem_zipWith
-- 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_3 :
  ∀ (hMl : l.length ≤ l.length) (hMs : IsGreatest s l.length) (hM_lt : l.length < L.length)
    (hM_ltx : l.length < (x :: l).length) (hM_lty : l.length < (l ++ [y]).length),
    d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (l ++ [y]) l.length hM_lty) y ≤ L.sum
refine_3₁ :
  ∀ (hMl : M < l.length), d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (l ++ [y]) M hM_lty) y ≤ L.sum
⊢ d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (l ++ [y]) M hM_lty) y ≤ L.sum

Tactic:
rcases hMl.eq_or_lt with (rfl | hMl)

Premises used: LE.le.eq_or_lt, rfl
-- 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 : l.length ≤ l.length
hMs : IsGreatest s l.length
hM_lt : l.length < L.length
hM_ltx : l.length < (x :: l).length
hM_lty : l.length < (l ++ [y]).length
⊢ d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (l ++ [y]) l.length hM_lty) y ≤ L.sum

Tactic:
simp only [getElem_append_right le_rfl, getElem_singleton, dist_self, zero_le]

Premises used: zero_le, List.getElem_singleton, le_rfl, List.getElem_append_right
-- 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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
refine_3 : d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) l M hMl) y ≤ L.sum
⊢ d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (l ++ [y]) M hM_lty) y ≤ L.sum

Tactic:
rw [getElem_append_left hMl]

Premises used: List.getElem_append_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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
⊢ (drop (M + 1) l).length = l.length - (M + 1)

Tactic:
have hlen : length (drop (M + 1) l) = length l - (M + 1) := length_drop
-- 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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
⊢ l.length - (M + 1) < l.length

Tactic:
have hlen_lt : length l - (M + 1) < length l := Nat.sub_lt_of_pos_le M.succ_pos hMl
-- 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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
⊢ d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) l M hMl) y ≤ L.sum

Tactic:
(ihn _ hlen_lt _ y _ hlen).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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
refine_3 :
  2 *
      (zipWith d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) l M hMl :: drop (M + 1) l)
          (drop (M + 1) l ++ [y])).sum ≤
    L.sum
⊢ d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) l M hMl) y ≤ L.sum

Tactic:
refine (ihn _ hlen_lt _ y _ hlen).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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
refine_3 : 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
⊢ 2 *
      (zipWith d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) l M hMl :: drop (M + 1) l)
          (drop (M + 1) l ++ [y])).sum ≤
    L.sum

Tactic:
rw [cons_getElem_drop_succ]

Premises used: List.cons_getElem_drop_succ
-- 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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
⊢ L.sum ≤ 2 * (take (M + 1) L).sum

Tactic:
have hMs' : L.sum ≤ 2 * (L.take (M + 1)).sum :=
      not_lt.1 fun h => (hMs.2 h.le).not_gt M.lt_succ_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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs' : L.sum ≤ 2 * (take (M + 1) L).sum
⊢ (drop (M + 1) L).sum ≤ (take (M + 1) L).sum

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

Premises used: add_le_add_iff_left, two_mul, add_le_add_iff_right, List.sum_take_add_sum_drop, HAdd.hAdd, OfNat.ofNat
-- 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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs' : L.sum ≤ 2 * (take (M + 1) L).sum
hMs'₁ : (drop (M + 1) L).sum ≤ (take (M + 1) L).sum
⊢ 2 * (drop (M + 1) L).sum ≤ L.sum

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

Premises used: add_le_add_iff_left, two_mul, add_le_add_iff_right, List.sum_take_add_sum_drop, HAdd.hAdd, OfNat.ofNat
-- 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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs'_1 : (drop (M + 1) L).sum ≤ (take (M + 1) L).sum
hMs' : 2 * (drop (M + 1) L).sum ≤ L.sum
⊢ 2 * (drop (M + 1) L).sum ≤ L.sum

Tactic:
hMs'
-- 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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs'_1 : (drop (M + 1) L).sum ≤ (take (M + 1) L).sum
hMs' : 2 * (drop (M + 1) L).sum ≤ L.sum
h : zipWith d (drop M l) (drop (M + 1) l ++ [y]) = drop (M + 1) L
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum

Tactic:
convert! hMs'
-- 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_1 : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs'_1 : (drop (M + 1) L).sum ≤ (take (M + 1) L).sum
hMs' : 2 * (drop (M + 1) L).sum ≤ L.sum
h : zipWith d (drop M l) (drop (M + 1) l ++ [y]) = zipWith d (drop (M + 1) (x :: l)) (drop (M + 1) (l ++ [y]))
h₁ : zipWith d (drop M l) (drop (M + 1) l ++ [y]) = zipWith d (drop M l) (drop (M + 1) (l ++ [y]))
h₂ : zipWith d (drop M l) (drop (M + 1) l ++ [y]) = zipWith d (drop M l) (drop (M + 1) l ++ [y])
h₃ : M + 1 ≤ l.length
h₄ : zipWith d (drop M l) (drop (M + 1) l ++ [y]) = zipWith d (drop M l) (drop (M + 1) l ++ [y])
h₅ h₆ h₇ : M + 1 ≤ l.length
⊢ zipWith d (drop M l) (drop (M + 1) l ++ [y]) = drop (M + 1) L

Tactic:
rwa [drop_zipWith, drop, drop_append_of_le_length]

Premises used: List.drop_zipWith, List.drop_append_of_le_length, List.drop
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
rcases :
  ∀ (V : ℕ → SetRel X X) (hB : (𝓤 X).HasAntitoneBasis V) (hV_symm : ∀ (n : ℕ), (V n).IsSymm),
    ∃ (U : ℕ → SetRel X X),
      (∀ (n : ℕ), (U n).IsSymm) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U
⊢ ∃ (U : ℕ → SetRel X X),
    (∀ (n : ℕ), (U n).IsSymm) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U

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

Premises used: UniformSpace.has_seq_basis
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hB : (𝓤 X).HasAntitoneBasis V
hV_symm : ∀ (n : ℕ), (V n).IsSymm
rcases :
  ∀ (φ : ℕ → ℕ) (hφ_comp : ∀ ⦃m n : ℕ⦄, m < n → (fun (x : SetRel X X) ↦ V (φ n) ○ x)^[2] (V (φ n)) ⊆ V (φ m))
    (hφB : (𝓤 X).HasAntitoneBasis (V ∘ φ)),
    ∃ (U : ℕ → SetRel X X),
      (∀ (n : ℕ), (U n).IsSymm) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U
⊢ ∃ (U : ℕ → SetRel X X),
    (∀ (n : ℕ), (U n).IsSymm) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U

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

Premises used: Filter.HasAntitoneBasis.mem, eventually_uniformity_iterate_comp_subset, Filter.HasAntitoneBasis.subbasis_with_rel, Filter.Tendsto.eventually, OfNat.ofNat, Filter.HasAntitoneBasis.tendsto_smallSets
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hB : (𝓤 X).HasAntitoneBasis V
hV_symm : ∀ (n : ℕ), (V n).IsSymm
φ : ℕ → ℕ
hφ_comp : ∀ ⦃m n : ℕ⦄, m < n → (fun (x : SetRel X X) ↦ V (φ n) ○ x)^[2] (V (φ n)) ⊆ V (φ m)
hφB : (𝓤 X).HasAntitoneBasis (V ∘ φ)
⊢ ∃ (U : ℕ → SetRel X X),
    (∀ (n : ℕ), (U n).IsSymm) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U

Tactic:
⟨V ∘ φ, fun n => hV_symm _, hφ_comp, hφB⟩

Premises used: Function.comp, And.intro, Exists.intro
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hB : (𝓤 X).HasAntitoneBasis V
hV_symm : ∀ (n : ℕ), (V n).IsSymm
φ : ℕ → ℕ
hφ_comp : ∀ ⦃m n : ℕ⦄, m < n → (fun (x : SetRel X X) ↦ V (φ n) ○ x)^[2] (V (φ n)) ⊆ V (φ m)
hφB : (𝓤 X).HasAntitoneBasis (V ∘ φ)
⊢ ∃ (U : ℕ → SetRel X X),
    (∀ (n : ℕ), (U n).IsSymm) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U

Tactic:
exact ⟨V ∘ φ, fun n => hV_symm _, hφ_comp, hφB⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
obtain :
  ∀ (U : ℕ → SetRel X X) (hU_symm : ∀ (n : ℕ), (U n).IsSymm) (hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m)
    (hB : (𝓤 X).HasAntitoneBasis U), ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst
⊢ ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst

Tactic:
obtain ⟨U, hU_symm, hU_comp, hB⟩ :
    ∃ U : ℕ → SetRel X X,
      (∀ n, (U n).IsSymm) ∧
        (∀ ⦃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⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
x y : X
⊢ d x y = 0 ↔ Inseparable x y

Tactic:
Iff.trans ?_ hB.inseparable_iff_uniformity.symm

Premises used: Filter.HasAntitoneBasis.toHasBasis, Iff.trans, Iff.symm, Filter.HasBasis.inseparable_iff_uniformity