awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
h₂ : n + 1 + m = m + (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)))

Tactic:
convert!
          Finset.sum_Ico_add (fun i : ℕ => edist (f (w (i + 1))) (f (w i))) 0 m (n + 1) using 3

Premises used: Finset.sum_Ico_add, HAdd.hAdd, EDist.edist, OfNat.ofNat
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))
⊢ n + 1 = 0 + (n + 1)

Tactic:
abel
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))
⊢ n + 1 + m = m + (n + 1)

Tactic:
abel
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)))
rw₁ : Disjoint (Finset.range n) (Finset.Ico (n + 1) (n + 1 + m))
⊢ 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:
rw [← Finset.sum_union]

Premises used: Finset.sum_union
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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₁ : Finset.range n ∪ Finset.Ico (n + 1) (n + 1 + m) ⊆ Finset.range (n + 1 + m)
⊢ 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:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))
⊢ Finset.range n ∪ Finset.Ico (n + 1) (n + 1 + m) ⊆ Finset.range (n + 1 + m)

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))
⊢ ∀ ⦃a : ℕ⦄, a ∈ Finset.range n → a ∉ Finset.Ico (n + 1) (n + 1 + m)

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))
⊢ Disjoint (Finset.range n) (Finset.Ico (n + 1) (n + 1 + m))

Tactic:
exact Finset.disjoint_left.2 (by grind)

Premises used: Iff.mpr, Finset.disjoint_left
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))
⊢ Monotone w

Tactic:
grind [Monotone]

Premises used: Monotone
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ), w i ∈ s ∪ t

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
apply : eVariationOn f (s ∪ t) ≤ eVariationOn f s + eVariationOn f t
⊢ 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'

Premises used: eVariationOn.add_le_union, LE.le.antisymm', And.right, LE.le.trans
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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

Tactic:
iSup_le fun ⟨n, ⟨u, hu, ust⟩⟩ ↦ ?_

Premises used: LE.le, eVariationOn, Prod.fst, Finset.range, HAdd.hAdd, iSup_le, _private.0.eVariationOn.union.match_1, EDist.edist, OfNat.ofNat, Subtype.val, Prod.snd, Finset.sum
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
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 ⋯).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
⊢ eVariationOn f (s ∪ t) ≤ eVariationOn f s + eVariationOn f t

Tactic:
refine iSup_le fun ⟨n, ⟨u, hu, ust⟩⟩ ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
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 ⋯).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
⊢ ∑ 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

Tactic:
obtain ⟨v, m, hv, vst, ⟨N, hN, rfl⟩, huv⟩ :=
    eVariationOn.add_point f (mem_union_left t hs.1) u hu ust n

Premises used: eVariationOn.add_point, And.left, Set.mem_union_left, rfl
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
apply : ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)) ≤ eVariationOn f s + eVariationOn f 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

Tactic:
apply huv.trans

Premises used: LE.le.trans
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
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
⊢ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)) ≤ eVariationOn f s + eVariationOn f t

Tactic:
rw [Finset.range_eq_Ico, ← Finset.sum_Ico_consecutive _ zero_le hN.le]

Premises used: zero_le, LT.lt.le, Finset.sum_Ico_consecutive, Finset.range_eq_Ico
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
h₂ : ∑ i ∈ Finset.Ico N m, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f t
⊢ 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:
apply add_le_add

Premises used: add_le_add
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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

Tactic:
sum_le_of_monotoneOn_Icc (hv.monotoneOn _) fun i hi ↦ ?_

Premises used: eVariationOn.sum_le_of_monotoneOn_Icc, Monotone.monotoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ) (hi : i ∈ Icc 0 N), v i ∈ s
⊢ ∑ i ∈ Finset.Ico 0 N, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f s

Tactic:
refine sum_le_of_monotoneOn_Icc (hv.monotoneOn _) fun i hi ↦ ?_

Premises used: eVariationOn.sum_le_of_monotoneOn_Icc, Monotone.monotoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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

Tactic:
sum_le_of_monotoneOn_Icc (hv.monotoneOn _) fun i hi ↦ ?_

Premises used: eVariationOn.sum_le_of_monotoneOn_Icc, Monotone.monotoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ) (hi : i ∈ Icc N m), v i ∈ t
⊢ ∑ i ∈ Finset.Ico N m, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f t

Tactic:
refine sum_le_of_monotoneOn_Icc (hv.monotoneOn _) fun i hi ↦ ?_

Premises used: eVariationOn.sum_le_of_monotoneOn_Icc, Monotone.monotoneOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ
hi : i ∈ Icc 0 N
⊢ v i ∈ s

Tactic:
(vst i).elim id (fun h ↦ (hv hi.2).antisymm (ht.2 h) ▸ hs.1)

Premises used: LE.le.antisymm, Eq.rec, id, And.right, And.left, Or.elim, Eq.symm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ
hi : i ∈ Icc 0 N
⊢ v i ∈ s

Tactic:
exact (vst i).elim id (fun h ↦ (hv hi.2).antisymm (ht.2 h) ▸ hs.1)

Premises used: LE.le.antisymm, Eq.rec, id, And.right, And.left, Or.elim, Eq.symm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ
hi : i ∈ Icc N m
⊢ v i ∈ t

Tactic:
(vst i).elim (fun h ↦ (hs.2 h).antisymm (hv hi.1) ▸ ht.1) id

Premises used: LE.le.antisymm, Eq.rec, id, And.right, And.left, Or.elim, Eq.symm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : ℕ
hi : i ∈ Icc N m
⊢ v i ∈ t

Tactic:
exact (vst i).elim (fun h ↦ (hs.2 h).antisymm (hv hi.1) ▸ ht.1) id

Premises used: id, Or.elim
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ 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⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ 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⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
rw₂ rw₃ : eVariationOn f (s ∩ Icc a 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)

Tactic:
rw [← eVariationOn.union f A B, ← inter_union_distrib_left, Icc_union_Icc_eq_Icc hab hbc]

Premises used: Set.Icc_union_Icc_eq_Icc, eVariationOn.union, Set.inter_union_distrib_left
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
hn : ∀ (i : ℕ), 0 < i → i < 0 → E i ∈ s
⊢ ∑ i ∈ Finset.range 0, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E 0))

Tactic:
simp [eVariationOn.subsingleton f Subsingleton.inter_singleton]

Premises used: eVariationOn.subsingleton, Set.Subsingleton.inter_singleton
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)))
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)))
⊢ ∑ 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
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)))

Tactic:
simp [hn₀]
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
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)))
neg₁ : E 0 ≤ E n
neg₂ : E n ≤ E (n + 1)
neg₃ : E n ∈ s
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))

Tactic:
rw [← Icc_add_Icc (b := E n)]

Premises used: eVariationOn.Icc_add_Icc