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)
hw : Monotone w
Npos : 0 < N
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)))
⊢ ∑ 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₁ : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.Ico N n, edist (f (w (1 + i + 1))) (f (w (1 + i))))
  (∑ i ∈ Finset.Ico (N + 1) (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
⊢ ∑ 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)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)))
        (∑ i ∈ Finset.Ico (N - 1) (N + 1), edist (f (w (i + 1))) (f (w i))) +
      ∑ i ∈ Finset.Ico (N + 1) (n + 1), edist (f (w (i + 1))) (f (w i))
have refine : edist (f (w (N + 1))) (f (w (N - 1))) ≤ ∑ i ∈ Finset.Ico (N - 1) (N + 1), edist (f (w (i + 1))) (f (w i))
Tactic: refine add_le_add (add_le_add le_rfl ?_) le_rfl
-- 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
⊢ 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 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 (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
⊢ 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 B : N - 1 + 1 < N + 1
Tactic: have B : N - 1 + 1 < N + 1 := A.symm ▸ N.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)
hw : Monotone w
Npos : 0 < N
A : N - 1 + 1 = N
B : N - 1 + 1 < N + 1
⊢ 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 C : N - 1 < N + 1
Tactic: have C : N - 1 < N + 1 := lt_of_le_of_lt N.pred_le N.lt_succ_self
-- 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
B : N - 1 + 1 < N + 1
C : N - 1 < N + 1
⊢ 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 rw : edist (f (w (N + 1))) (f (w (N - 1))) ≤ edist (f (w (N + 1))) (f (w N)) + edist (f (w N)) (f (w (N - 1)))
Tactic: rw [Finset.sum_eq_sum_Ico_succ_bot C, Finset.sum_eq_sum_Ico_succ_bot B, A, Finset.Ico_self,
          Finset.sum_empty, add_zero, add_comm (edist _ _)]
-- 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 (w (i + 1))) (f (w i)))
        (∑ i ∈ Finset.Ico (N - 1) (N + 1), edist (f (w (i + 1))) (f (w i))) +
      ∑ i ∈ Finset.Ico (N + 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 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 + 1
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)))
        (∑ i ∈ Finset.Ico (N - 1) (N + 1), edist (f (w (i + 1))) (f (w i))) +
      ∑ i ∈ Finset.Ico (N + 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 hnk : N + 1 ≤ 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 + 1
hnk : N + 1 ≤ n + 1
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)))
        (∑ i ∈ Finset.Ico (N - 1) (N + 1), edist (f (w (i + 1))) (f (w i))) +
      ∑ i ∈ Finset.Ico (N + 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 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 + 1
hnk : N + 1 ≤ n + 1
hmn₁ : 0 ≤ N - 1
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i)))
        (∑ i ∈ Finset.Ico (N - 1) (N + 1), edist (f (w (i + 1))) (f (w i))) +
      ∑ i ∈ Finset.Ico (N + 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 hnk₁ : N - 1 ≤ 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
⊢ 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 : ∑ 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))
Tactic: calc
      (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
          ((∑ 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)) := by
        rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico] <;> grind
      _ = (∑ 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))) := by
        congr 1
        · congr 1
          · grind [Finset.sum_congr]
          · have A : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
            have : Finset.Ico (N - 1) N = {N - 1} := by rw [← Nat.Ico_succ_singleton, A]
            simp only [this, A, Finset.sum_singleton]
        · grind [Finset.sum_congr]
      _ = (∑ 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)) := by
        congr 1
        · grind
        · exact Finset.sum_Ico_add (fun i => edist (f (w (i + 1))) (f (w i))) N n 1
      _ ≤ ((∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i))) +
              ∑ i ∈ Finset.Ico (N - 1) (N + 1), edist (f (w (i + 1))) (f (w i))) +
            ∑ i ∈ Finset.Ico (N + 1) (n + 1), edist (f (w (i + 1))) (f (w i)) := by
        refine add_le_add (add_le_add le_rfl ?_) le_rfl
        have A : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
        have B : N - 1 + 1 < N + 1 := A.symm ▸ N.lt_succ_self
        have C : N - 1 < N + 1 := lt_of_le_of_lt N.pred_le N.lt_succ_self
        rw [Finset.sum_eq_sum_Ico_succ_bot C, Finset.sum_eq_sum_Ico_succ_bot B, A, Finset.Ico_self,
          Finset.sum_empty, add_zero, add_comm (edist _ _)]
        exact edist_triangle _ _ _
      _ = ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)) := by
        rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico] <;> 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
have pos : ∀ (hs : s = ∅), eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
Tactic: by_cases hs : s = ∅
-- 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
pos : ∀ (hs : s = ∅), eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
have neg : ∀ (hs : ¬s = ∅), eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
Tactic: by_cases hs : s = ∅
-- 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
have this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
Tactic: have : Nonempty { u // Monotone u ∧ ∀ i : ℕ, u i ∈ s } :=
    nonempty_monotone_mem (nonempty_iff_ne_empty.2 hs)
-- 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
have pos : ∀ (ht : t = ∅), eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
Tactic: by_cases ht : t = ∅
-- 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
pos : ∀ (ht : t = ∅), eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
have neg : ∀ (ht : ¬t = ∅), eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
Tactic: by_cases ht : t = ∅
-- 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
have this₁ : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
Tactic: have : Nonempty { u // Monotone u ∧ ∀ i : ℕ, u i ∈ t } :=
    nonempty_monotone_mem (nonempty_iff_ne_empty.2 ht)
-- 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this_1 : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
have neg : ∀ (i : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }) (j : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }),
  HAdd.hAdd (α := ℝ≥0∞) (∑ i_1 ∈ Finset.range i.1, edist (f ((↑i.2 : ℕ → α) (i_1 + 1))) (f ((↑i.2 : ℕ → α) i_1)))
      (∑ i ∈ Finset.range j.1, edist (f ((↑j.2 : ℕ → α) (i + 1))) (f ((↑j.2 : ℕ → α) i))) ≤
    eVariationOn f (s ∪ t)
Tactic: refine ENNReal.iSup_add_iSup_le ?_
-- 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this_1 : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
      (∑ i ∈ Finset.range m, edist (f (v (i + 1))) (f (v i))) =
    HAdd.hAdd (α := ℝ≥0∞)
      (∑ i ∈ Finset.range n,
        edist (f (if i + 1 ≤ n then u (i + 1) else v (i + 1 - (n + 1)))) (f (if i ≤ n then u i else v (i - (n + 1)))))
      (∑ i ∈ Finset.range m,
        edist (f (if n + 1 + i + 1 ≤ n then u (n + 1 + i + 1) else v (n + 1 + i + 1 - (n + 1))))
          (f (if n + 1 + i ≤ n then u (n + 1 + i) else v (n + 1 + i - (n + 1)))))
have e_a : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
  (∑ i ∈ Finset.range n,
    edist (f (if i + 1 ≤ n then u (i + 1) else v (i + 1 - (n + 1)))) (f (if i ≤ n then u i else v (i - (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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this_1 : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else v (i - (n + 1))
e_a :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
    (∑ i ∈ Finset.range n,
      edist (f (if i + 1 ≤ n then u (i + 1) else v (i + 1 - (n + 1)))) (f (if i ≤ n then u i else v (i - (n + 1)))))
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
      (∑ i ∈ Finset.range m, edist (f (v (i + 1))) (f (v i))) =
    HAdd.hAdd (α := ℝ≥0∞)
      (∑ i ∈ Finset.range n,
        edist (f (if i + 1 ≤ n then u (i + 1) else v (i + 1 - (n + 1)))) (f (if i ≤ n then u i else v (i - (n + 1)))))
      (∑ i ∈ Finset.range m,
        edist (f (if n + 1 + i + 1 ≤ n then u (n + 1 + i + 1) else v (n + 1 + i + 1 - (n + 1))))
          (f (if n + 1 + i ≤ n then u (n + 1 + i) else v (n + 1 + i - (n + 1)))))
have e_a₁ : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range m, edist (f (v (i + 1))) (f (v i)))
  (∑ i ∈ Finset.range m,
    edist (f (if n + 1 + i + 1 ≤ n then u (n + 1 + i + 1) else v (n + 1 + i + 1 - (n + 1))))
      (f (if n + 1 + i ≤ n then u (n + 1 + i) else v (n + 1 + i - (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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this_1 : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (w (i + 1))) (f (w i)))
      (∑ i ∈ Finset.range m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i)))) =
    HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (w (i + 1))) (f (w i)))
      (∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i)))
have e_a : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))))
  (∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this_1 : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))))
    (∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i)))
have e_a : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))))
  (∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this_1 : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))))
    (∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i)))
have h₁ : n + 1 = 0 + (n + 1)
Tactic: convert!
          Finset.sum_Ico_add (fun i : ℕ => edist (f (w (i + 1))) (f (w i))) 0 m (n + 1) using 3
-- 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this_1 : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else v (i - (n + 1))
h₁ : n + 1 = 0 + (n + 1)
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))))
    (∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i)))
have h₂ : n + 1 + m = m + (n + 1)
Tactic: convert!
          Finset.sum_Ico_add (fun i : ℕ => edist (f (w (i + 1))) (f (w i))) 0 m (n + 1) using 3
-- 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this_1 : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (w (i + 1))) (f (w i)))
      (∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i))) ≤
    ∑ i ∈ Finset.range (n + 1 + m), edist (f (w (i + 1))) (f (w i))
have rw : LE.le (α := ℝ≥0∞) (∑ x ∈ Finset.range n ∪ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (x + 1))) (f (w x)))
  (∑ i ∈ Finset.range (n + 1 + m), edist (f (w (i + 1))) (f (w i)))
Tactic: rw [← Finset.sum_union]