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 : 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
⊢ 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:
grind [Finset.sum_congr]

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

Tactic:
congr 1
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 0 (N - 1), edist (f (w (i + 1))) (f (w i)) + edist (f (w (N + 1))) (f (w (N - 1)))

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ 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:
Finset.sum_Ico_add (fun i => edist (f (w (i + 1))) (f (w i))) N n 1

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 : 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
⊢ 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:
exact Finset.sum_Ico_add (fun i => edist (f (w (i + 1))) (f (w i))) N n 1

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 : 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))

Tactic:
add_le_add (add_le_add le_rfl ?_) le_rfl

Premises used: le_rfl, 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 : 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
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))
⊢ ∑ 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))

Tactic:
refine add_le_add (add_le_add le_rfl ?_) le_rfl

Premises used: le_rfl, 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 : 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
⊢ N - 1 + 1 < N + 1

Tactic:
have B : N - 1 + 1 < N + 1 := A.symm ▸ N.lt_succ_self
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ N - 1 < N + 1

Tactic:
have C : N - 1 < N + 1 := lt_of_le_of_lt N.pred_le N.lt_succ_self
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
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)))
⊢ 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:
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 _ _)]

Premises used: Finset.Ico_self, add_comm, Finset.sum_eq_sum_Ico_succ_bot, Finset.sum_empty, EDist.edist, add_zero
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))) ≤ edist (f (w (N + 1))) (f (w N)) + edist (f (w N)) (f (w (N - 1)))

Tactic:
edist_triangle _ _ _

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))) ≤ edist (f (w (N + 1))) (f (w N)) + edist (f (w N)) (f (w (N - 1)))

Tactic:
exact edist_triangle _ _ _

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

Tactic:
rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico]

Premises used: 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 : 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
⊢ 0 ≤ N + 1

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ N + 1 ≤ n + 1

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ N - 1 ≤ N + 1

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
pos : ∀ (hs : s = ∅), eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
neg : ∀ (hs : ¬s = ∅), eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)

Tactic:
by_cases hs : s = ∅
-- 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 = ∅
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)

Tactic:
simp [hs]
-- 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 = ∅
⊢ 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)
-- 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 : 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)
neg : ∀ (ht : ¬t = ∅), eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)

Tactic:
by_cases ht : t = ∅
-- 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 : 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)

Tactic:
simp [ht]
-- 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 : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
⊢ 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)
-- 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 }
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)

Tactic:
ENNReal.iSup_add_iSup_le ?_

Premises used: ENNReal.iSup_add_iSup_le, eVariationOn
-- 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 }
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)
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)

Tactic:
refine ENNReal.iSup_add_iSup_le ?_

Premises used: ENNReal.iSup_add_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 α
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))
dsimp :
  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)))))
⊢ 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:
dsimp only [w]
-- 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))
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)))))
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)))))
⊢ 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)))))

Tactic:
congr 1
-- 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))
⊢ 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:
grind [Finset.sum_congr]

Premises used: Finset.sum_congr
-- 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))
⊢ 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:
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))
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)))
⊢ 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:
congr 1
-- 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))
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)))
⊢ 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:
rw [Finset.range_eq_Ico]

Premises used: 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 α
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∞) (∑ x ∈ Finset.Ico 0 m, edist (f (w (n + 1 + x + 1))) (f (w (n + 1 + x))))
    (∑ x ∈ Finset.Ico (0 + (n + 1)) (m + (n + 1)), edist (f (w (x + 1))) (f (w x)))

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

Premises used: Finset.sum_Ico_add, HAdd.hAdd, EDist.edist, OfNat.ofNat