-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem add_le_union (f : α → E) {s t : Set α} (h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) :
    eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { 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 : ℕ → α := fun i => if i ≤ n then u i else v (i - (n + 1))
wst : ∀ (i : ℕ), w i ∈ s ∪ t
i j : ℕ
hij : i ≤ j
⊢ (if i ≤ n then u i else v (i - (n + 1))) ≤ if j ≤ n then u j else v (j - (n + 1))

Tactic:
split_ifs with h_1 h_2 h_2

Result:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { 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 : ℕ → α := fun i => if i ≤ n then u i else v (i - (n + 1))
wst : ∀ (i : ℕ), w i ∈ s ∪ t
i j : ℕ
hij : i ≤ j
h_1 : i ≤ n
h_2 : j ≤ n
⊢ u i ≤ u j

case neg
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { 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 : ℕ → α := fun i => if i ≤ n then u i else v (i - (n + 1))
wst : ∀ (i : ℕ), w i ∈ s ∪ t
i j : ℕ
hij : i ≤ j
h_1 : i ≤ n
h_2 : ¬j ≤ n
⊢ u i ≤ v (j - (n + 1))

case pos
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { 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 : ℕ → α := fun i => if i ≤ n then u i else v (i - (n + 1))
wst : ∀ (i : ℕ), w i ∈ s ∪ t
i j : ℕ
hij : i ≤ j
h_1 : ¬i ≤ n
h_2 : j ≤ n
⊢ v (i - (n + 1)) ≤ u j

case neg
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { 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 : ℕ → α := fun i => if i ≤ n then u i else v (i - (n + 1))
wst : ∀ (i : ℕ), w i ∈ s ∪ t
i j : ℕ
hij : i ≤ j
h_1 : ¬i ≤ n
h_2 : ¬j ≤ n
⊢ v (i - (n + 1)) ≤ v (j - (n + 1))

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { 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 : ℕ → α := fun i => if i ≤ n then u i else v (i - (n + 1))
wst : ∀ (i : ℕ), w i ∈ s ∪ t
hw : Monotone w
⊢ ∑ 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)))

Tactic:
dsimp only [w]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { 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 : ℕ → α := fun i => if i ≤ n then u i else v (i - (n + 1))
wst : ∀ (i : ℕ), w i ∈ s ∪ t
hw : Monotone w
⊢ ∑ 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 (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))))

Proof state:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { 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 : ℕ → α := fun i => if i ≤ n then u i else v (i - (n + 1))
wst : ∀ (i : ℕ), w i ∈ s ∪ t
hw : Monotone w
i : ℕ
hi : n + 1 ≤ i ∧ i < n + 1 + m
⊢ i < n + 1 + m

Tactic:
exact hi.2

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { 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 : ℕ → α := fun i => if i ≤ n then u i else v (i - (n + 1))
wst : ∀ (i : ℕ), w i ∈ s ∪ t
hw : Monotone w
i : ℕ
hi : i ∈ Finset.range n
h'i : i ∈ Finset.Ico (n + 1) (n + 1 + m)
⊢ False

Tactic:
simp only [Finset.mem_Ico, Finset.mem_range] at hi h'i

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { 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 : ℕ → α := fun i => if i ≤ n then u i else v (i - (n + 1))
wst : ∀ (i : ℕ), w i ∈ s ∪ t
hw : Monotone w
i : ℕ
hi : i < n
h'i : n + 1 ≤ i ∧ i < n + 1 + m
⊢ False

Proof state:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { 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 : ℕ → α := fun i => if i ≤ n then u i else v (i - (n + 1))
wst : ∀ (i : ℕ), w i ∈ s ∪ t
i j : ℕ
hij : i ≤ j
h_1 : i ≤ n
h_2 : j ≤ n
⊢ u i ≤ u j

Tactic:
exact hu hij

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : t = ∅
⊢ eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)

Tactic:
simp [ht]

Result:
no goals