E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
⊢ False
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ SatelliteConfig E (multiplicity E) (goodτ E) → False
intro a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
b : SatelliteConfig E (multiplicity E) (goodτ E) := SatelliteConfig.centerAndRescale a
⊢ False
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
⊢ False
let b := a.centerAndRescale
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
b : SatelliteConfig E (multiplicity E) (goodτ E) := SatelliteConfig.centerAndRescale a
c' : Fin (Nat.succ (multiplicity E)) → E
c'_le_two : ∀ (n : Fin (Nat.succ (multiplicity E))), ‖c' n‖ ≤ 2
hc' : ∀ (i j : Fin (Nat.succ (multiplicity E))), i ≠ j → 1 - goodδ E ≤ ‖c' i - c' j‖
⊢ False
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
b : SatelliteConfig E (multiplicity E) (goodτ E) := SatelliteConfig.centerAndRescale a
⊢ False
rcases b.exists_normalized a.centerAndRescale_center a.centerAndRescale_radius
    (one_lt_goodτ E).le (goodδ E) le_rfl (goodδ_lt_one E).le with
  ⟨c', c'_le_two, hc'⟩
no goals
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
b : SatelliteConfig E (multiplicity E) (goodτ E) := SatelliteConfig.centerAndRescale a
c' : Fin (Nat.succ (multiplicity E)) → E
c'_le_two : ∀ (n : Fin (Nat.succ (multiplicity E))), ‖c' n‖ ≤ 2
hc' : ∀ (i j : Fin (Nat.succ (multiplicity E))), i ≠ j → 1 - goodδ E ≤ ‖c' i - c' j‖
⊢ False
exact
  lt_irrefl _ ((Nat.lt_succ_self _).trans_le (le_multiplicity_of_δ_of_fin c' c'_le_two hc'))