awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
inl : ∀ (hi : i + 1 < N), w i ≤ w (i + 1)
inr : ∀ (hi : i + 1 = N), w i ≤ w (i + 1)
⊢ w i ≤ w (i + 1)
have inr₁ : ∀ (hi : N < i + 1), w i ≤ w (i + 1)
Tactic: rcases lt_trichotomy (i + 1) N with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : i + 1 = N
⊢ w i ≤ w (i + 1)
have A : i < N
Tactic: have A : i < N := hi ▸ i.lt_succ_self
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : i + 1 = N
A : i < N
⊢ w i ≤ w (i + 1)
have this : ¬(i ≤ n ∧ x < u i)
Tactic: have := Nat.find_min exists_N A
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
⊢ ∃ (v : ℕ → α) (m : ℕ),
    Monotone v ∧
      (∀ (i : ℕ), v i ∈ s) ∧
        x ∈ v '' Iio m ∧
          LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
            (∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)))
have hw : Monotone w
Tactic: have hw : Monotone w := by
    apply monotone_nat_of_le_succ fun i => ?_
    rcases lt_trichotomy (i + 1) N with (hi | hi | hi)
    · grind [Monotone]
    · have A : i < N := hi ▸ i.lt_succ_self
      have := Nat.find_min exists_N A
      grind
    · grind [Monotone]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
⊢ ∃ (v : ℕ → α) (m : ℕ),
    Monotone v ∧
      (∀ (i : ℕ), v i ∈ s) ∧
        x ∈ v '' Iio m ∧
          LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
            (∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)))
have inr : LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
  (∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)))
Tactic: refine ⟨w, n + 1, hw, by grind, (mem_image _ _ _).2 ⟨N, by grind⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)))
have inr : ∀ (Npos : N = 0),
  LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)))
Tactic: rcases eq_zero_or_pos N with (Npos | Npos)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
inr :
  ∀ (Npos : N = 0),
    LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
      (∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)))
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)))
have inr₁ : ∀ (Npos : 0 < N),
  LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)))
Tactic: rcases eq_zero_or_pos N with (Npos | Npos)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : N = 0
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i))))
    (∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)))
have rw : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 n, edist (f (w (1 + i + 1))) (f (w (1 + i))))
  (∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)))
Tactic: rw [Finset.range_eq_Ico]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : N = 0
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)))
    (∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)))
have rw : LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)))
  (∑ j ∈ Finset.Ico 0 (n + 1), edist (f (w (j + 1))) (f (w j)))
Tactic: rw [Finset.range_eq_Ico]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : N = 0
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)))
    (∑ j ∈ Finset.Ico 0 (n + 1), edist (f (w (j + 1))) (f (w j)))
have h₁ : LE.le (α := ℕ) 0 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : N = 0
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)))
have i : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
  (∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i))))
Tactic: calc
      (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
          ∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i))) := by grind
      _ = ∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)) := by
        rw [Finset.range_eq_Ico]
        exact Finset.sum_Ico_add (fun i => edist (f (w (i + 1))) (f (w i))) 0 n 1
      _ ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)) := by
        rw [Finset.range_eq_Ico]
        gcongr
        exact zero_le_one
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : N = 0
i :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i))))
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)))
have i₁ : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i))))
  (∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)))
Tactic: calc
      (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
          ∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i))) := by grind
      _ = ∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)) := by
        rw [Finset.range_eq_Ico]
        exact Finset.sum_Ico_add (fun i => edist (f (w (i + 1))) (f (w i))) 0 n 1
      _ ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)) := by
        rw [Finset.range_eq_Ico]
        gcongr
        exact zero_le_one
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : N = 0
i :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i))))
i₁ :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i))))
    (∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)))
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)))
have i₂ : LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)))
  (∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)))
Tactic: calc
      (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
          ∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i))) := by grind
      _ = ∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)) := by
        rw [Finset.range_eq_Ico]
        exact Finset.sum_Ico_add (fun i => edist (f (w (i + 1))) (f (w i))) 0 n 1
      _ ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)) := by
        rw [Finset.range_eq_Ico]
        gcongr
        exact zero_le_one
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
    HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
        (∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) +
      ∑ i ∈ Finset.Ico N n, edist (f (u (i + 1))) (f (u i))
have hmn : 0 ≤ N
Tactic: rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
hmn : 0 ≤ N
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
    HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
        (∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) +
      ∑ i ∈ Finset.Ico N n, edist (f (u (i + 1))) (f (u i))
have hnk : N ≤ n
Tactic: rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
hmn : 0 ≤ N
hnk : N ≤ n
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
    HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
        (∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) +
      ∑ i ∈ Finset.Ico N n, edist (f (u (i + 1))) (f (u i))
have hmn₁ : 0 ≤ N - 1
Tactic: rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
hmn : 0 ≤ N
hnk : N ≤ n
hmn₁ : 0 ≤ N - 1
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
    HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
        (∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) +
      ∑ i ∈ Finset.Ico N n, edist (f (u (i + 1))) (f (u i))
have hnk₁ : N - 1 ≤ N
Tactic: rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
        (∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) +
      ∑ i ∈ Finset.Ico N n, edist (f (u (i + 1))) (f (u i)) =
    ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (u N)) (f (u (N - 1))) +
      ∑ i ∈ Finset.Ico N n, edist (f (w (1 + i + 1))) (f (w (1 + i)))
have e_a : HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) =
  ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (u N)) (f (u (N - 1)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
e_a :
  HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
      (∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) =
    ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (u N)) (f (u (N - 1)))
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
        (∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) +
      ∑ i ∈ Finset.Ico N n, edist (f (u (i + 1))) (f (u i)) =
    ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (u N)) (f (u (N - 1))) +
      ∑ i ∈ Finset.Ico N n, edist (f (w (1 + i + 1))) (f (w (1 + i)))
have e_a₁ : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.Ico N n, edist (f (u (i + 1))) (f (u i)))
  (∑ i ∈ Finset.Ico N n, edist (f (w (1 + i + 1))) (f (w (1 + i))))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
      (∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) =
    ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (u N)) (f (u (N - 1)))
have e_a : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
  (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
e_a :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)))
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i)))
      (∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) =
    ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (u N)) (f (u (N - 1)))
have e_a₁ : ∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i)) = edist (f (u N)) (f (u (N - 1)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
⊢ ∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i)) = edist (f (u N)) (f (u (N - 1)))
have A : N - 1 + 1 = N
Tactic: have A : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
A : N - 1 + 1 = N
⊢ Finset.Ico (N - 1) N = {N - 1}
have rw : Finset.Ico (N - 1) N = Finset.Ico (N - 1) (N - 1 + 1)
Tactic: rw [← Nat.Ico_succ_singleton, A]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
A : N - 1 + 1 = N
rw : Finset.Ico (N - 1) N = Finset.Ico (N - 1) (N - 1 + 1)
⊢ Finset.Ico (N - 1) N = {N - 1}
have rw₁ : Finset.Ico (N - 1) N = Finset.Ico (N - 1) N
Tactic: rw [← Nat.Ico_succ_singleton, A]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
A : N - 1 + 1 = N
⊢ ∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i)) = edist (f (u N)) (f (u (N - 1)))
have this : Finset.Ico (N - 1) N = {N - 1}
Tactic: have : Finset.Ico (N - 1) N = {N - 1} := by rw [← Nat.Ico_succ_singleton, A]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n_1 ≤ n ∧ x < u n_1) exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun (i : ℕ) ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
⊢ ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (u N)) (f (u (N - 1))) +
      ∑ i ∈ Finset.Ico N n, edist (f (w (1 + i + 1))) (f (w (1 + i))) =
    ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (w (N + 1))) (f (w (N - 1))) +
      ∑ i ∈ Finset.Ico (N + 1) (n + 1), edist (f (w (i + 1))) (f (w i))
have e_a : ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (u N)) (f (u (N - 1))) =
  ∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (w (N + 1))) (f (w (N - 1)))
Tactic: congr 1