Theorem: uniformly_bounded_of_chain_ne_of_pathLength_le (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✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R : ℝ
⊢ ∃ n, ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ R → l.length ≤ n
Tactic:
have ⟨r, hr, hr'⟩ := exists_min_dist V
State after:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
⊢ ∃ n, ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ R → l.length ≤ n

State before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
⊢ ∃ n, ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ R → l.length ≤ n
Tactic:
refine ⟨⌊R / r + 1⌋₊, ?_⟩
State after:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
⊢ ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ R → l.length ≤ ⌊R / r + 1⌋₊

State before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
⊢ ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ R → l.length ≤ ⌊R / r + 1⌋₊
Tactic:
intro l hl hl'
State after:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
⊢ l.length ≤ ⌊R / r + 1⌋₊

State before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
⊢ l.length ≤ ⌊R / r + 1⌋₊
Tactic:
have hR : 0 ≤ R := l.pathLength_nonneg.trans hl'
State after:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
⊢ l.length ≤ ⌊R / r + 1⌋₊

State before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
⊢ l.length ≤ ⌊R / r + 1⌋₊
Tactic:
have := length_mul_le_pathLength_add hr.le hr' hl
State after:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ l.length ≤ ⌊R / r + 1⌋₊

State before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ l.length ≤ ⌊R / r + 1⌋₊
Tactic:
rw [Nat.le_floor_iff, div_add_one hr.ne', le_div_iff hr]
State after:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ ↑l.length * r ≤ R + r

V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ 0 ≤ R / r + 1

State before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ ↑l.length * r ≤ R + r
Tactic:
linarith
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✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ 0 ≤ R / r + 1
Tactic:
positivity
State after:
no goals