Theorem: length_mul_le_pathLength_add (LeanCamCombi/SylvesterChvatal.lean)

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x✝ : List.Chain' (fun x x_1 => x ≠ x_1) []
⊢ ↑[].length * r ≤ [].pathLength + r
Tactic:
simp [List.pathLength, hr]
State after:
no goals

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
head✝ : V
x✝ : List.Chain' (fun x x_1 => x ≠ x_1) [head✝]
⊢ ↑[head✝].length * r ≤ [head✝].pathLength + r
Tactic:
simp [List.pathLength]
State after:
no goals

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x y : V
xs : List V
h' : List.Chain' (fun x x_1 => x ≠ x_1) (x :: y :: xs)
⊢ ↑(x :: y :: xs).length * r ≤ (x :: y :: xs).pathLength + r
Tactic:
simp only [List.chain'_cons] at h'
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x y : V
xs : List V
h' : x ≠ y ∧ List.Chain' (fun x x_1 => x ≠ x_1) (y :: xs)
⊢ ↑(x :: y :: xs).length * r ≤ (x :: y :: xs).pathLength + r

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x y : V
xs : List V
h' : x ≠ y ∧ List.Chain' (fun x x_1 => x ≠ x_1) (y :: xs)
⊢ ↑(x :: y :: xs).length * r ≤ (x :: y :: xs).pathLength + r
Tactic:
rw [List.pathLength, List.length, Nat.cast_add_one, add_one_mul (α := ℝ), add_assoc,
  add_comm]
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x y : V
xs : List V
h' : x ≠ y ∧ List.Chain' (fun x x_1 => x ≠ x_1) (y :: xs)
⊢ r + ↑(y :: xs).length * r ≤ dist x y + ((y :: xs).pathLength + r)

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x y : V
xs : List V
h' : x ≠ y ∧ List.Chain' (fun x x_1 => x ≠ x_1) (y :: xs)
⊢ r + ↑(y :: xs).length * r ≤ dist x y + ((y :: xs).pathLength + r)
Tactic:
exact add_le_add (h _ _ h'.1) (length_mul_le_pathLength_add hr h h'.2)
State after:
no goals