awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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
⊢ d x (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (x :: l) M hM_ltx) ≤ L.sum
have 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
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]
Cleared hypotheses: M, hMl, hMs, hM_lt, hM_ltx, hM_lty
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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) (l ++ [y]) M hM_lty) y ≤ L.sum
have 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
Tactic: rcases hMl.eq_or_lt with (rfl | hMl)
Cleared hypotheses: M, hMl, hMs, hM_lt, hM_ltx, hM_lty
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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
⊢ d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (l ++ [y]) M hM_lty) y ≤ L.sum
have 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
Tactic: rcases hMl.eq_or_lt with (rfl | hMl)
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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
⊢ d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) (l ++ [y]) M hM_lty) y ≤ L.sum
have refine_3 : d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) l M hMl) y ≤ L.sum
Tactic: rw [getElem_append_left hMl]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (hypothesis)
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
⊢ d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) l M hMl) y ≤ L.sum
have hlen : (drop (M + 1) l).length = l.length - (M + 1)
Tactic: have hlen : length (drop (M + 1) l) = length l - (M + 1) := length_drop
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (hypothesis)
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)
⊢ d (getElem (valid := fun (as : List X) (i : ℕ) ↦ i < as.length) l M hMl) y ≤ L.sum
have hlen_lt : 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
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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
have 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
Tactic: refine (ihn _ hlen_lt _ y _ hlen).trans ?_
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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
⊢ 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
have refine_3 : 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
Tactic: rw [cons_getElem_drop_succ]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (hypothesis)
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
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
have hMs' : 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
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (hypothesis)
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
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
have hMs'₁ : (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'
Cleared hypotheses: hMs'
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (hypothesis)
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 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
have hMs'₂ : 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'
Cleared hypotheses: hMs'
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
have h : zipWith d (drop M l) (drop (M + 1) l ++ [y]) = drop (M + 1) L
Tactic: convert! hMs'
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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
⊢ zipWith d (drop M l) (drop (M + 1) l ++ [y]) = drop (M + 1) L
have h : zipWith d (drop M l) (drop (M + 1) l ++ [y]) = zipWith d (drop (M + 1) (x :: l)) (drop (M + 1) (l ++ [y]))
Tactic: rwa [drop_zipWith, drop, drop_append_of_le_length]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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]))
⊢ zipWith d (drop M l) (drop (M + 1) l ++ [y]) = drop (M + 1) L
have h₁ : zipWith d (drop M l) (drop (M + 1) l ++ [y]) = zipWith d (drop M l) (drop (M + 1) (l ++ [y]))
Tactic: rwa [drop_zipWith, drop, drop_append_of_le_length]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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]))
⊢ zipWith d (drop M l) (drop (M + 1) l ++ [y]) = drop (M + 1) L
have h₂ : zipWith d (drop M l) (drop (M + 1) l ++ [y]) = zipWith d (drop M l) (drop (M + 1) l ++ [y])
Tactic: rwa [drop_zipWith, drop, drop_append_of_le_length]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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])
⊢ zipWith d (drop M l) (drop (M + 1) l ++ [y]) = drop (M + 1) L
have h₃ : M + 1 ≤ l.length
Tactic: rwa [drop_zipWith, drop, drop_append_of_le_length]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
⊢ ∃ (U : ℕ → SetRel X X),
    (∀ (n : ℕ), (U n).IsSymm) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U
have 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
Tactic: rcases UniformSpace.has_seq_basis X with ⟨V, hB, hV_symm⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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
⊢ ∃ (U : ℕ → SetRel X X),
    (∀ (n : ℕ), (U n).IsSymm) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
⊢ ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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
have refine : d x y = 0 ↔ ∀ (i : ℕ), True → (x, y) ∈ U i
Tactic: refine Iff.trans ?_ hB.inseparable_iff_uniformity.symm
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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 ↔ ∀ (i : ℕ), True → (x, y) ∈ U i
have simp : Eq (α := ℝ≥0) (if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0) 0 ↔
  ∀ (i : ℕ), (x, y) ∈ U i
Tactic: simp only [d, true_imp_iff]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Uniformity (goal)
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
⊢ Eq (α := ℝ≥0) (if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0) 0 ↔
    ∀ (i : ℕ), (x, y) ∈ U i
have pos : ∀ (h : ∃ (n : ℕ), (x, y) ∉ U n), (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i
Tactic: split_ifs with h