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

case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
H : last N ≤ i
⊢ dist (c a i) (c a (last N)) ≤ r a i + r a (last N)
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
⊢ dist (c a i) (c a (last N)) ≤ r a i + r a (last N)
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 : i < last N
⊢ dist (c a i) (c a (last N)) ≤ r a i + r a (last N)
exact a.inter i H
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
H : last N ≤ i
I : i = last N
⊢ dist (c a i) (c a (last N)) ≤ r a i + r a (last N)
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
H : last N ≤ i
⊢ dist (c a i) (c a (last N)) ≤ r a i + r a (last N)
have I : 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 : last N ≤ i
I : i = last N
this : 0 ≤ r a (last N)
⊢ dist (c a i) (c a (last N)) ≤ r a i + r a (last N)
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
H : last N ≤ i
I : i = last N
⊢ dist (c a i) (c a (last N)) ≤ r a i + r a (last N)
have := (a.rpos (last N)).le
no goals
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin (Nat.succ N)
H : last N ≤ i
I : i = last N
this : 0 ≤ r a (last N)
⊢ dist (c a i) (c a (last N)) ≤ r a i + r a (last N)
simp only [I, add_nonneg this this, dist_self]