-- 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 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)
⊢ ∃ 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))

Tactic:
have ws : ∀ i, w i ∈ s := by
  dsimp only [w]
  intro i
  split_ifs
  exacts [us _, hx, us _]

Result:
case 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
⊢ ∃ 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 : ℕ
_hi : i ∈ Finset.range n
⊢ edist (f (u (i + 1))) (f (u i)) = edist (f (w (1 + i + 1))) (f (w (1 + i)))

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

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

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

case 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 ∈ 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))

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

Tactic:
exact zero_le _

Result:
no goals

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

Tactic:
exact hu (Nat.pred_le _)

Result:
no goals

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
⊢ edist (f (u N)) (f (u (N - 1))) = edist (f (w (N + 1))) (f (w (N - 1)))

Tactic:
dsimp only [w]

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

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
⊢ (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 := hi ▸ i.lt_succ_self

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
⊢ (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)