E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
have ah :
    ∀ i j, i ≠ j → a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨
      a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j := by
  simpa only [dist_eq_norm] using a.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
have δnonneg : 0 ≤ δ := by linarith only [hτ, hδ1]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
have D : 0 ≤ 1 - δ / 4 := by linarith only [hδ2]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
have τpos : 0 < τ := _root_.zero_lt_one.trans_le hτ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
have hcrj : ‖a.c j‖ ≤ a.r j + 1 := by simpa only [lastc, lastr, dist_zero_right] using a.inter' j
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
have J : (1 - δ / 4) * τ ≤ 1 :=
  calc
    (1 - δ / 4) * τ ≤ (1 - δ / 4) * (1 + δ / 4) := mul_le_mul_of_nonneg_left hδ1 D
    _ = (1 : ℝ) - δ ^ 2 / 16 := by ring
    _ ≤ 1 := by linarith only [sq_nonneg δ]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
⊢ 1 - δ ≤ ‖c a i - d‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : r a j - δ ≤ ‖c a i - c a j‖
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
set d := (2 / ‖a.c j‖) • a.c j with hd
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
this : r a j - δ ≤ ‖c a i - d‖ + (r a j - 1)
⊢ 1 - δ ≤ ‖c a i - d‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
⊢ 1 - δ ≤ ‖c a i - d‖
have : a.r j - δ ≤ ‖a.c i - d‖ + (a.r j - 1) :=
  calc
    a.r j - δ ≤ ‖a.c i - a.c j‖ := A
    _ ≤ ‖a.c i - d‖ + ‖d - a.c j‖ := by simp only [← dist_eq_norm, dist_triangle]
    _ ≤ ‖a.c i - d‖ + (a.r j - 1) := by
      apply add_le_add_left
      have A : 0 ≤ 1 - 2 / ‖a.c j‖ := by simpa [div_le_iff (zero_le_two.trans_lt hj)] using hj.le
      rw [← one_smul ℝ (a.c j), hd, ← sub_smul, norm_smul, norm_sub_rev, Real.norm_eq_abs,
        abs_of_nonneg A, sub_mul]
      field_simp [(zero_le_two.trans_lt hj).ne']
      linarith only [hcrj]
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
this : r a j - δ ≤ ‖c a i - d‖ + (r a j - 1)
⊢ 1 - δ ≤ ‖c a i - d‖
linarith only [this]
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
⊢ ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
simpa only [dist_eq_norm] using a.h
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ 0 ≤ δ
linarith only [hτ, hδ1]
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
⊢ 0 ≤ 1 - δ / 4
linarith only [hδ2]
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
⊢ ‖c a j‖ ≤ r a j + 1
simpa only [lastc, lastr, dist_zero_right] using a.inter' j
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
H : i < last N
⊢ r a i ≤ 2

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
H : last N ≤ i
⊢ r a i ≤ 2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
⊢ r a i ≤ 2
rcases lt_or_le i (last N) with (H | H)
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
H : i < last N
⊢ dist (c a i) (c a (last N)) ≤ 2
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
H : i < last N
⊢ r a i ≤ 2
apply (a.hlast i H).1.trans
no goals
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
H : i < last N
⊢ dist (c a i) (c a (last N)) ≤ 2
simpa only [dist_eq_norm, lastc, sub_zero] using hi
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
H : last N ≤ i
this : i = last N
⊢ r a i ≤ 2
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
H : last N ≤ i
⊢ r a i ≤ 2
have : i = last N := top_le_iff.1 H
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
H : last N ≤ i
this : i = last N
⊢ 1 ≤ 2
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
H : last N ≤ i
this : i = last N
⊢ r a i ≤ 2
rw [this, lastr]
no goals
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
H : last N ≤ i
this : i = last N
⊢ 1 ≤ 2
exact one_le_two
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
⊢ (1 - δ / 4) * (1 + δ / 4) = 1 - δ ^ 2 / 16
ring
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
⊢ 1 - δ ^ 2 / 16 ≤ 1
linarith only [sq_nonneg δ]
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ r a j - δ ≤ ‖c a i - c a j‖

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
⊢ r a j - δ ≤ ‖c a i - c a j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
⊢ r a j - δ ≤ ‖c a i - c a j‖
rcases ah j i inej.symm with (H | H)
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ r a j - δ ≤ ‖c a i - c a j‖
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
⊢ r a j - δ ≤ ‖c a i - c a j‖
have C : a.r j ≤ 4 :=
  calc
    a.r j ≤ τ * a.r i := H.2
    _ ≤ τ * 2 := (mul_le_mul_of_nonneg_left I τpos.le)
    _ ≤ 5 / 4 * 2 := (mul_le_mul_of_nonneg_right (by linarith only [hδ1, hδ2]) zero_le_two)
    _ ≤ 4 := by norm_num
no goals
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ r a j - δ ≤ ‖c a i - c a j‖
calc
  a.r j - δ ≤ a.r j - a.r j / 4 * δ := by
    refine' sub_le_sub le_rfl _
    refine' mul_le_of_le_one_left δnonneg _
    linarith only [C]
  _ = (1 - δ / 4) * a.r j := by ring
  _ ≤ (1 - δ / 4) * (τ * a.r i) := (mul_le_mul_of_nonneg_left H.2 D)
  _ ≤ 1 * a.r i := by rw [← mul_assoc]; apply mul_le_mul_of_nonneg_right J (a.rpos _).le
  _ ≤ ‖a.c i - a.c j‖ := by rw [one_mul]; exact H.1
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ r a j - δ ≤ ‖c a j - c a i‖
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ r a j - δ ≤ ‖c a i - c a j‖
rw [norm_sub_rev]
no goals
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ r a j - δ ≤ ‖c a j - c a i‖
linarith [H.1]
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
⊢ τ ≤ 5 / 4
linarith only [hδ1, hδ2]
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
⊢ 5 / 4 * 2 ≤ 4
norm_num
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ r a j / 4 * δ ≤ δ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ r a j - δ ≤ r a j - r a j / 4 * δ
refine' sub_le_sub le_rfl _
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ r a j / 4 ≤ 1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ r a j / 4 * δ ≤ δ
refine' mul_le_of_le_one_left δnonneg _
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ r a j / 4 ≤ 1
linarith only [C]
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ r a j - r a j / 4 * δ = (1 - δ / 4) * r a j
ring
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ (1 - δ / 4) * τ * r a i ≤ 1 * r a i
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ (1 - δ / 4) * (τ * r a i) ≤ 1 * r a i
rw [← mul_assoc]
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ (1 - δ / 4) * τ * r a i ≤ 1 * r a i
apply mul_le_mul_of_nonneg_right J (a.rpos _).le
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ r a i ≤ ‖c a i - c a j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ 1 * r a i ≤ ‖c a i - c a j‖
rw [one_mul]
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
C : r a j ≤ 4
⊢ r a i ≤ ‖c a i - c a j‖
exact H.1
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
⊢ ‖c a i - c a j‖ ≤ ‖c a i - d‖ + ‖d - c a j‖
simp only [← dist_eq_norm, dist_triangle]
case bc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
⊢ ‖d - c a j‖ ≤ r a j - 1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
⊢ ‖c a i - d‖ + ‖d - c a j‖ ≤ ‖c a i - d‖ + (r a j - 1)
apply add_le_add_left
case bc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A✝ : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
A : 0 ≤ 1 - 2 / ‖c a j‖
⊢ ‖d - c a j‖ ≤ r a j - 1
case bc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
⊢ ‖d - c a j‖ ≤ r a j - 1
have A : 0 ≤ 1 - 2 / ‖a.c j‖ := by simpa [div_le_iff (zero_le_two.trans_lt hj)] using hj.le
case bc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A✝ : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
A : 0 ≤ 1 - 2 / ‖c a j‖
⊢ 1 * ‖c a j‖ - 2 / ‖c a j‖ * ‖c a j‖ ≤ r a j - 1
case bc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A✝ : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
A : 0 ≤ 1 - 2 / ‖c a j‖
⊢ ‖d - c a j‖ ≤ r a j - 1
rw [← one_smul ℝ (a.c j), hd, ← sub_smul, norm_smul, norm_sub_rev, Real.norm_eq_abs,
  abs_of_nonneg A, sub_mul]
case bc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A✝ : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
A : 0 ≤ 1 - 2 / ‖c a j‖
⊢ ‖c a j‖ ≤ r a j - 1 + 2
case bc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A✝ : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
A : 0 ≤ 1 - 2 / ‖c a j‖
⊢ 1 * ‖c a j‖ - 2 / ‖c a j‖ * ‖c a j‖ ≤ r a j - 1
field_simp [(zero_le_two.trans_lt hj).ne']
no goals
case bc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A✝ : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
A : 0 ≤ 1 - 2 / ‖c a j‖
⊢ ‖c a j‖ ≤ r a j - 1 + 2
linarith only [hcrj]
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
hi : ‖c a i‖ ≤ 2
hj : 2 < ‖c a j‖
ah :
  ∀ (i j : Fin (Nat.succ N)),
    i ≠ j → r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i ∨ r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
hcrj : ‖c a j‖ ≤ r a j + 1
I : r a i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : r a j - δ ≤ ‖c a i - c a j‖
d : E := (2 / ‖c a j‖) • c a j
hd : d = (2 / ‖c a j‖) • c a j
⊢ 0 ≤ 1 - 2 / ‖c a j‖
simpa [div_le_iff (zero_le_two.trans_lt hj)] using hj.le