E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ 1 <
    1 +
      Exists.choose
          (_ :
            ∃ δ,
              0 < δ ∧
                δ < 1 ∧
                  ∀ (s : Finset E),
                    (∀ (c : E), c ∈ s → ‖c‖ ≤ 2) →
                      (∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 - δ ≤ ‖c - d‖) →
                        Finset.card s ≤ multiplicity E) /
        4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ 1 < goodτ E
dsimp [goodτ, goodδ]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ 1 <
    1 +
      Exists.choose
          (_ :
            ∃ δ,
              0 < δ ∧
                δ < 1 ∧
                  ∀ (s : Finset E),
                    (∀ (c : E), c ∈ s → ‖c‖ ≤ 2) →
                      (∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 - δ ≤ ‖c - d‖) →
                        Finset.card s ≤ multiplicity E) /
        4
linarith [(exists_goodδ E).choose_spec.1]