E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 - c a j‖
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ j
⊢ 1 - δ ≤ ‖c a i - 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
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 - c a j‖
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 - c a j‖
have δnonneg : 0 ≤ δ := by linarith only [hτ, hδ1]
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 - c a j‖
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 - c a j‖
have D : 0 ≤ 1 - δ / 4 := by linarith only [hδ2]
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 - c a j‖
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 - c a j‖
have τpos : 0 < τ := _root_.zero_lt_one.trans_le hτ
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
⊢ 1 - δ ≤ ‖c a i - c a j‖
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 - c a j‖
have I : (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
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
⊢ 1 - δ ≤ ‖c a i - c a j‖
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
⊢ 1 - δ ≤ ‖c a i - c a j‖
have J : 1 - δ ≤ 1 - δ / 4 := by linarith only [δnonneg]
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
⊢ 1 - δ ≤ ‖c a i - c a j‖
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
⊢ 1 - δ ≤ ‖c a i - c a j‖
have K : 1 - δ / 4 ≤ τ⁻¹ := by rw [inv_eq_one_div, le_div_iff τpos]; exact I
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
L : τ⁻¹ ≤ ‖c a i - c a j‖
⊢ 1 - δ ≤ ‖c a i - c a j‖

case L
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
⊢ τ⁻¹ ≤ ‖c a i - c a j‖
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
⊢ 1 - δ ≤ ‖c a i - c a j‖
suffices L : τ⁻¹ ≤ ‖a.c i - a.c j‖
case L
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
⊢ τ⁻¹ ≤ ‖c a i - c a j‖
case L
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
⊢ τ⁻¹ ≤ ‖c a i - c a j‖
have hτ' : ∀ k, τ⁻¹ ≤ a.r k := by
  intro k
  rw [inv_eq_one_div, div_le_iff τpos, ← lastr, mul_comm]
  exact a.hlast' k hτ
case L.inl
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
⊢ τ⁻¹ ≤ ‖c a i - c a j‖

case L.inr
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
H : r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ τ⁻¹ ≤ ‖c a i - c a j‖
case L
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
⊢ τ⁻¹ ≤ ‖c a i - c a j‖
rcases ah i j inej with (H | H)
no goals
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 - δ / 4) * (1 + δ / 4) = 1 - δ ^ 2 / 16
ring
no goals
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 - δ ^ 2 / 16 ≤ 1
linarith only [sq_nonneg δ]
no goals
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
⊢ 1 - δ ≤ 1 - δ / 4
linarith only [δnonneg]
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
⊢ (1 - δ / 4) * τ ≤ 1
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
⊢ 1 - δ / 4 ≤ τ⁻¹
rw [inv_eq_one_div, le_div_iff τpos]
no goals
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
⊢ (1 - δ / 4) * τ ≤ 1
exact I
no goals
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
L : τ⁻¹ ≤ ‖c a i - c a j‖
⊢ 1 - δ ≤ ‖c a i - c a j‖
linarith only [J, K, L]
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
k : Fin (Nat.succ N)
⊢ τ⁻¹ ≤ r a k
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
⊢ ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
intro k
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
k : Fin (Nat.succ N)
⊢ r a (last N) ≤ τ * r a k
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
k : Fin (Nat.succ N)
⊢ τ⁻¹ ≤ r a k
rw [inv_eq_one_div, div_le_iff τpos, ← lastr, mul_comm]
no goals
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
k : Fin (Nat.succ N)
⊢ r a (last N) ≤ τ * r a k
exact a.hlast' k hτ
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
⊢ τ⁻¹ ≤ r a i
case L.inl
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
⊢ τ⁻¹ ≤ ‖c a i - c a j‖
apply le_trans _ H.1
no goals
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
H : r a i ≤ ‖c a i - c a j‖ ∧ r a j ≤ τ * r a i
⊢ τ⁻¹ ≤ r a i
exact hτ' i
case L.inr
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
H : r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ τ⁻¹ ≤ ‖c a j - c a i‖
case L.inr
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
H : r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ τ⁻¹ ≤ ‖c a i - c a j‖
rw [norm_sub_rev]
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
H : r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ τ⁻¹ ≤ r a j
case L.inr
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
H : r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ τ⁻¹ ≤ ‖c a j - c a i‖
apply le_trans _ H.1
no goals
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin (Nat.succ N)
inej : i ≠ 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 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin (Nat.succ N)), τ⁻¹ ≤ r a k
H : r a j ≤ ‖c a j - c a i‖ ∧ r a i ≤ τ * r a j
⊢ τ⁻¹ ≤ r a j
exact hτ' j