-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem add_point (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ → α) (hu : Monotone u)
    (us : ∀ i, u i ∈ s) (n : ℕ) :
    ∃ (v : ℕ → α) (m : ℕ), Monotone v ∧ (∀ i, v i ∈ s) ∧ x ∈ v '' Iio m ∧
      (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) ≤
        ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
hw : Monotone w
Npos : 0 < N
⊢ ∑ 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))

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

Result:
case hmn
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
hw : Monotone w
Npos : 0 < N
⊢ 0 ≤ N

case hnk
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
hw : Monotone w
Npos : 0 < N
⊢ N ≤ n

case hmn
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
hw : Monotone w
Npos : 0 < N
⊢ 0 ≤ N - 1

case hnk
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
hw : Monotone w
Npos : 0 < N
⊢ N - 1 ≤ N

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
hw : Monotone w
Npos : 0 = N
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
    ∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i)))

Tactic:
apply Finset.sum_congr rfl fun i _hi => ?_

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
hw : Monotone w
Npos : 0 = N
i : ℕ
_hi : i ∈ Finset.range n
⊢ edist (f (u (i + 1))) (f (u i)) = edist (f (w (1 + i + 1))) (f (w (1 + i)))

Proof state:
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
i : ℕ
hi : N < i + 1
A : ¬i < N
B : ¬i + 1 < N
C : ¬i + 1 = N
D : i + 1 - 1 = i
⊢ (if i = N then x else u (i - 1)) ≤ u i

Tactic:
split_ifs

Result:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
i : ℕ
hi : N < i + 1
A : ¬i < N
B : ¬i + 1 < N
C : ¬i + 1 = N
D : i + 1 - 1 = i
h✝ : i = N
⊢ x ≤ u i

case neg
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
i : ℕ
hi : N < i + 1
A : ¬i < N
B : ¬i + 1 < N
C : ¬i + 1 = N
D : i + 1 - 1 = i
h✝ : ¬i = N
⊢ u (i - 1) ≤ u i

Proof state:
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
i : ℕ
hi : N < i + 1
⊢ (if i < N then u i else if i = N then x else u (i - 1)) ≤
    if i + 1 < N then u (i + 1) else if i + 1 = N then x else u (i + 1 - 1)

Tactic:
have A : ¬i < N := (Nat.lt_succ_iff.mp hi).not_lt

Result:
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
i : ℕ
hi : N < i + 1
A : ¬i < N
⊢ (if i < N then u i else if i = N then x else u (i - 1)) ≤
    if i + 1 < N then u (i + 1) else if i + 1 = N then x else u (i + 1 - 1)

Proof state:
case e_a.e_a.e_a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)
ws : ∀ (i : ℕ), w i ∈ s
hw : Monotone w
Npos : 0 < N
i : ℕ
hi : N ≤ i ∧ i < n
A : ¬1 + i + 1 < N
B : ¬1 + i + 1 = N
C : ¬1 + i < N
D : ¬1 + i = N
⊢ i = (i + 1).pred

Tactic:
apply Nat.pred_succ

Result:
no goals