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

Tactic:
have : Finset.Ico (N - 1) N = {N - 1} := by rw [← Nat.Ico_succ_singleton, A]

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

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 : u n ≤ x
v : ℕ → α := fun i => if i ≤ n then u i else x
i : ℕ
h✝ : i ≤ n
⊢ u i ∈ s

Tactic:
exact us i

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)
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 (u (1 + i))) (f (u i))

Tactic:
rw [add_comm 1 i]

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)
ws : ∀ (i : ℕ), w i ∈ s
hw : Monotone w
Npos : 0 < N
i : ℕ
hi : N ≤ i ∧ i < n
⊢ ¬1 + i + 1 < N

Tactic:
omega

Result:
no goals

Proof state:
case inr.inl
α : 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 : i + 1 = N
A : i < N
B : ¬i + 1 < N
T : ¬(i ≤ n ∧ x < u i)
⊢ u i ≤ x

Tactic:
push_neg at T

Result:
case inr.inl
α : 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 : i + 1 = N
A : i < N
B : ¬i + 1 < N
T : i ≤ n → u i ≤ x
⊢ u i ≤ x

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
A : N - 1 + 1 = N
⊢ 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:
have B : N - 1 + 1 < N + 1 := A.symm ▸ N.lt_succ_self

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
A : N - 1 + 1 = N
B : N - 1 + 1 < 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))

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
⊢ (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 D : i + 1 - 1 = i := Nat.pred_succ i

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

Tactic:
simp only [A, not_and, not_lt, Nat.succ_ne_self, Nat.add_succ_sub_one, add_zero,
  if_false, B, if_true]

Result:
no goals