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 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))
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)))
⊢ 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₁ : Disjoint (Finset.range n) (Finset.Ico (n + 1) (n + 1 + m))
Tactic: rw [← Finset.sum_union]
-- 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))
⊢ 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)))
have h₁ : Finset.range n ∪ Finset.Ico (n + 1) (n + 1 + m) ⊆ Finset.range (n + 1 + m)
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 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, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
        edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
          (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i)))
      (∑ i ∈ Finset.range (m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).1,
        edist (f ((↑(m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).2 : ℕ → α) (i + 1)))
          (f ((↑(m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).2 : ℕ → α) i))) ≤
    eVariationOn f (s ∪ t)
have i : 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 (w (i + 1))) (f (w i)))
    (∑ i ∈ Finset.range m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))))
Tactic: calc
    ((∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) +
          ∑ i ∈ Finset.range m, edist (f (v (i + 1))) (f (v i))) =
        (∑ 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))) := by
      dsimp only [w]
      congr 1
      · grind [Finset.sum_congr]
      · grind
    _ = (∑ 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)) := by
      congr 1
      rw [Finset.range_eq_Ico]
      convert!
          Finset.sum_Ico_add (fun i : ℕ => edist (f (w (i + 1))) (f (w i))) 0 m (n + 1) using 3 <;>
        abel
    _ ≤ ∑ i ∈ Finset.range (n + 1 + m), edist (f (w (i + 1))) (f (w i)) := by
      rw [← Finset.sum_union]
      · gcongr; grind
      · exact Finset.disjoint_left.2 (by grind)
    _ ≤ eVariationOn f (s ∪ t) := sum_le (by grind [Monotone]) (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 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))
i :
  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 (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, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
        edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
          (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i)))
      (∑ i ∈ Finset.range (m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).1,
        edist (f ((↑(m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).2 : ℕ → α) (i + 1)))
          (f ((↑(m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).2 : ℕ → α) i))) ≤
    eVariationOn f (s ∪ t)
have i₁ : 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)))
Tactic: calc
    ((∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) +
          ∑ i ∈ Finset.range m, edist (f (v (i + 1))) (f (v i))) =
        (∑ 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))) := by
      dsimp only [w]
      congr 1
      · grind [Finset.sum_congr]
      · grind
    _ = (∑ 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)) := by
      congr 1
      rw [Finset.range_eq_Ico]
      convert!
          Finset.sum_Ico_add (fun i : ℕ => edist (f (w (i + 1))) (f (w i))) 0 m (n + 1) using 3 <;>
        abel
    _ ≤ ∑ i ∈ Finset.range (n + 1 + m), edist (f (w (i + 1))) (f (w i)) := by
      rw [← Finset.sum_union]
      · gcongr; grind
      · exact Finset.disjoint_left.2 (by grind)
    _ ≤ eVariationOn f (s ∪ t) := sum_le (by grind [Monotone]) (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 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))
i :
  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 (w (i + 1))) (f (w i)))
      (∑ i ∈ Finset.range m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))))
i₁ :
  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)))
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
        edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
          (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i)))
      (∑ i ∈ Finset.range (m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).1,
        edist (f ((↑(m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).2 : ℕ → α) (i + 1)))
          (f ((↑(m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).2 : ℕ → α) i))) ≤
    eVariationOn f (s ∪ t)
have 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))) ≤
  ∑ i ∈ Finset.range (n + 1 + m), 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 m, edist (f (v (i + 1))) (f (v i))) =
        (∑ 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))) := by
      dsimp only [w]
      congr 1
      · grind [Finset.sum_congr]
      · grind
    _ = (∑ 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)) := by
      congr 1
      rw [Finset.range_eq_Ico]
      convert!
          Finset.sum_Ico_add (fun i : ℕ => edist (f (w (i + 1))) (f (w i))) 0 m (n + 1) using 3 <;>
        abel
    _ ≤ ∑ i ∈ Finset.range (n + 1 + m), edist (f (w (i + 1))) (f (w i)) := by
      rw [← Finset.sum_union]
      · gcongr; grind
      · exact Finset.disjoint_left.2 (by grind)
    _ ≤ eVariationOn f (s ∪ t) := sum_le (by grind [Monotone]) (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 t : Set α
x : α
hs : IsGreatest s x
ht : IsLeast t x
⊢ eVariationOn f (s ∪ t) = eVariationOn f s + eVariationOn f t
have apply : eVariationOn f (s ∪ t) ≤ eVariationOn f s + eVariationOn f t
Tactic: apply (eVariationOn.add_le_union f fun a ha b hb ↦ (hs.2 ha).trans (ht.2 hb)).antisymm'
-- 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 α
x : α
hs : IsGreatest s x
ht : IsLeast t x
⊢ eVariationOn f (s ∪ t) ≤ eVariationOn f s + eVariationOn f t
have refine : ∀ (x : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t }) (n : ℕ) (u : ℕ → α) (hu : Monotone u)
  (ust : ∀ (i : ℕ), u i ∈ s ∪ t),
  ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u sorry).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u sorry).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u sorry).2 : ℕ → α) i)) ≤
    eVariationOn f s + eVariationOn f t
Tactic: refine iSup_le fun ⟨n, ⟨u, hu, ust⟩⟩ ↦ ?_
-- 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 α
x : α
hs : IsGreatest s x
ht : IsLeast t x
x_1 : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t }
n : ℕ
u : ℕ → α
hu : Monotone u
ust : ∀ (i : ℕ), u i ∈ s ∪ t
⊢ ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u ⋯).2 : ℕ → α) i)) ≤
    eVariationOn f s + eVariationOn f t
have obtain : ∀ (v : ℕ → α) (m : ℕ) (hv : Monotone v) (vst : ∀ (i : ℕ), v i ∈ s ∪ t)
  (huv :
    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))))
  (N : ℕ) (hN : N ∈ Iio m) (hs : IsGreatest s (v N)) (ht : IsLeast t (v N)),
  ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u sorry).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u sorry).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u sorry).2 : ℕ → α) i)) ≤
    eVariationOn f s + eVariationOn f t
Tactic: obtain ⟨v, m, hv, vst, ⟨N, hN, rfl⟩, huv⟩ :=
    eVariationOn.add_point f (mem_union_left t hs.1) u hu ust n
Cleared hypotheses: x, hs, 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 α
x : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t }
n : ℕ
u : ℕ → α
hu : Monotone u
ust : ∀ (i : ℕ), u i ∈ s ∪ t
v : ℕ → α
m : ℕ
hv : Monotone v
vst : ∀ (i : ℕ), v i ∈ s ∪ t
huv :
  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)))
N : ℕ
hN : N ∈ Iio m
hs : IsGreatest s (v N)
ht : IsLeast t (v N)
⊢ ∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u ⋯).1,
      edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u ⋯).2 : ℕ → α) (i + 1)))
        (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t) u ⋯).2 : ℕ → α) i)) ≤
    eVariationOn f s + eVariationOn f t
have apply : ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)) ≤ eVariationOn f s + eVariationOn f t
Tactic: apply huv.trans
-- 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 α
x : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t }
n : ℕ
u : ℕ → α
hu : Monotone u
ust : ∀ (i : ℕ), u i ∈ s ∪ t
v : ℕ → α
m : ℕ
hv : Monotone v
vst : ∀ (i : ℕ), v i ∈ s ∪ t
huv :
  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)))
N : ℕ
hN : N ∈ Iio m
hs : IsGreatest s (v N)
ht : IsLeast t (v N)
⊢ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)) ≤ eVariationOn f s + eVariationOn f t
have rw : HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 N, edist (f (v (i + 1))) (f (v i)))
    (∑ i ∈ Finset.Ico N m, edist (f (v (i + 1))) (f (v i))) ≤
  eVariationOn f s + eVariationOn f t
Tactic: rw [Finset.range_eq_Ico, ← Finset.sum_Ico_consecutive _ zero_le hN.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 α
x : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t }
n : ℕ
u : ℕ → α
hu : Monotone u
ust : ∀ (i : ℕ), u i ∈ s ∪ t
v : ℕ → α
m : ℕ
hv : Monotone v
vst : ∀ (i : ℕ), v i ∈ s ∪ t
huv :
  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)))
N : ℕ
hN : N ∈ Iio m
hs : IsGreatest s (v N)
ht : IsLeast t (v N)
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 N, edist (f (v (i + 1))) (f (v i)))
      (∑ i ∈ Finset.Ico N m, edist (f (v (i + 1))) (f (v i))) ≤
    eVariationOn f s + eVariationOn f t
have h₁ : ∑ i ∈ Finset.Ico 0 N, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f s
Tactic: apply add_le_add
-- 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 α
x : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t }
n : ℕ
u : ℕ → α
hu : Monotone u
ust : ∀ (i : ℕ), u i ∈ s ∪ t
v : ℕ → α
m : ℕ
hv : Monotone v
vst : ∀ (i : ℕ), v i ∈ s ∪ t
huv :
  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)))
N : ℕ
hN : N ∈ Iio m
hs : IsGreatest s (v N)
ht : IsLeast t (v N)
h₁ : ∑ i ∈ Finset.Ico 0 N, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f s
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.Ico 0 N, edist (f (v (i + 1))) (f (v i)))
      (∑ i ∈ Finset.Ico N m, edist (f (v (i + 1))) (f (v i))) ≤
    eVariationOn f s + eVariationOn f t
have h₂ : ∑ i ∈ Finset.Ico N m, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f t
Tactic: apply add_le_add
-- 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 α
x : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t }
n : ℕ
u : ℕ → α
hu : Monotone u
ust : ∀ (i : ℕ), u i ∈ s ∪ t
v : ℕ → α
m : ℕ
hv : Monotone v
vst : ∀ (i : ℕ), v i ∈ s ∪ t
huv :
  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)))
N : ℕ
hN : N ∈ Iio m
hs : IsGreatest s (v N)
ht : IsLeast t (v N)
⊢ ∑ i ∈ Finset.Ico 0 N, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f s
have h₁ : ∀ (i : ℕ) (hi : i ∈ Icc 0 N), v i ∈ s
Tactic: refine sum_le_of_monotoneOn_Icc (hv.monotoneOn _) fun i hi ↦ ?_
-- 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 α
x : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t }
n : ℕ
u : ℕ → α
hu : Monotone u
ust : ∀ (i : ℕ), u i ∈ s ∪ t
v : ℕ → α
m : ℕ
hv : Monotone v
vst : ∀ (i : ℕ), v i ∈ s ∪ t
huv :
  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)))
N : ℕ
hN : N ∈ Iio m
hs : IsGreatest s (v N)
ht : IsLeast t (v N)
⊢ ∑ i ∈ Finset.Ico N m, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f t
have h₂ : ∀ (i : ℕ) (hi : i ∈ Icc N m), v i ∈ t
Tactic: refine sum_le_of_monotoneOn_Icc (hv.monotoneOn _) fun i 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 α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
have A : IsGreatest (s ∩ Icc a b) b
Tactic: have A : IsGreatest (s ∩ Icc a b) b :=
    ⟨⟨hb, hab, le_rfl⟩, inter_subset_right.trans Icc_subset_Iic_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 α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
A : IsGreatest (s ∩ Icc a b) b
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
have B : IsLeast (s ∩ Icc b c) b
Tactic: have B : IsLeast (s ∩ Icc b c) b :=
    ⟨⟨hb, le_rfl, hbc⟩, inter_subset_right.trans Icc_subset_Ici_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 α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
A : IsGreatest (s ∩ Icc a b) b
B : IsLeast (s ∩ Icc b c) b
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
have rw : eVariationOn f (s ∩ Icc a b ∪ s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
Tactic: rw [← eVariationOn.union f A B, ← inter_union_distrib_left, Icc_union_Icc_eq_Icc hab hbc]
-- 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 α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
A : IsGreatest (s ∩ Icc a b) b
B : IsLeast (s ∩ Icc b c) b
rw : eVariationOn f (s ∩ Icc a b ∪ s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
have rw₁ : eVariationOn f (s ∩ (Icc a b ∪ Icc b c)) = eVariationOn f (s ∩ Icc a c)
Tactic: rw [← eVariationOn.union f A B, ← inter_union_distrib_left, Icc_union_Icc_eq_Icc hab hbc]
-- 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 α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
A : IsGreatest (s ∩ Icc a b) b
B : IsLeast (s ∩ Icc b c) b
rw : eVariationOn f (s ∩ Icc a b ∪ s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
rw₁ : eVariationOn f (s ∩ (Icc a b ∪ Icc b c)) = eVariationOn f (s ∩ Icc a c)
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
have rw₂ : eVariationOn f (s ∩ Icc a c) = eVariationOn f (s ∩ Icc a c)
Tactic: rw [← eVariationOn.union f A B, ← inter_union_distrib_left, Icc_union_Icc_eq_Icc hab hbc]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))
have pos : ∀ (hn₀ : n = 0),
  ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))
Tactic: by_cases hn₀ : n = 0
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
pos :
  ∀ (hn₀ : n = 0),
    ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))
have neg : ∀ (hn₀ : ¬n = 0),
  ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))
Tactic: by_cases hn₀ : n = 0
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f : α → E_1
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  ∀ (hn : ∀ (i : ℕ), 0 < i → i < n → E i ∈ s),
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))
have neg : ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) =
  eVariationOn f (s ∩ Icc (E 0) (E n)) + eVariationOn f (s ∩ Icc (E n) (E (n + 1)))
Tactic: rw [← Icc_add_Icc (b := E n)]