-- 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:
case 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
A : N - 1 + 1 = N
this : Finset.Ico (N - 1) N = {N - 1}
⊢ ∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i)) = edist (f (u N)) (f (u (N - 1)))

Tactic:
simp only [this, A, Finset.sum_singleton]

Result:
no goals

Proof state:
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

Tactic:
exact hN.2.le.trans (hu (le_of_not_lt A))

Result:
no goals

Proof state:
case inr.refine_1
α : 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
⊢ (if N < N then u N else if N = N then x else u (N - 1)) = x

Tactic:
rw [if_neg (lt_irrefl N), if_pos rfl]

Result:
no goals

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)
⊢ ∀ (i : ℕ), w i ∈ s

Tactic:
dsimp only [w]

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)
⊢ ∀ (i : ℕ), (if i < N then u i else if i = N then x else u (i - 1)) ∈ s

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.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]

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 + 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 + 1

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 + 1

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 : ℕ
hi : N ≤ i ∧ i < n
A : ¬1 + i + 1 < N
B : ¬1 + i + 1 = N
C : ¬1 + i < N
D : ¬1 + i = N
⊢ edist (f (u (i + 1))) (f (u i)) =
    edist (f (if 1 + i + 1 < N then u (1 + i + 1) else if 1 + i + 1 = N then x else u (1 + i + 1 - 1)))
      (f (if 1 + i < N then u (1 + i) else if 1 + i = N then x else u (1 + i - 1)))

Tactic:
rw [if_neg A, if_neg B, if_neg C, if_neg D]

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 : N ≤ i ∧ i < n
A : ¬1 + i + 1 < N
B : ¬1 + i + 1 = N
C : ¬1 + i < N
D : ¬1 + i = N
⊢ edist (f (u (i + 1))) (f (u i)) = edist (f (u (1 + i + 1 - 1))) (f (u (1 + i - 1)))

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 : u n ≤ x
v : ℕ → α := fun i => if i ≤ n then u i else x
vs : ∀ (i : ℕ), v i ∈ s
⊢ Monotone v

Tactic:
refine monotone_nat_of_le_succ fun i => ?_

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 : u n ≤ x
v : ℕ → α := fun i => if i ≤ n then u i else x
vs : ∀ (i : ℕ), v i ∈ s
i : ℕ
⊢ v i ≤ v (i + 1)