case inl
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
h : 1 ≤ τ
H : i < last N
⊢ r a (last N) ≤ τ * r a i

case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
h : 1 ≤ τ
H : last N ≤ i
⊢ r a (last N) ≤ τ * r a i
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
h : 1 ≤ τ
⊢ r a (last N) ≤ τ * r a i
rcases lt_or_le i (last N) with (H | H)
no goals
case inl
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
h : 1 ≤ τ
H : i < last N
⊢ r a (last N) ≤ τ * r a i
exact (a.hlast i H).2
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ r a (last N) ≤ τ * r a i
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
h : 1 ≤ τ
H : last N ≤ i
⊢ r a (last N) ≤ τ * r a i
have : i = last N := top_le_iff.1 H
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ r a (last N) ≤ τ * r a (last N)
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ r a (last N) ≤ τ * r a i
rw [this]
no goals
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ r a (last N) ≤ τ * r a (last N)
exact le_mul_of_one_le_left (a.rpos _).le h