case h₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Nonempty
    {N |
      ∃ s, Finset.card s = N ∧ (∀ (c : E), c ∈ s → ‖c‖ ≤ 2) ∧ ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖}

case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ ∀ (b : ℕ),
    b ∈
        {N |
          ∃ s,
            Finset.card s = N ∧
              (∀ (c : E), c ∈ s → ‖c‖ ≤ 2) ∧ ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖} →
      b ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ multiplicity E ≤ 5 ^ finrank ℝ E
apply csSup_le
no goals
case h₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Nonempty
    {N |
      ∃ s, Finset.card s = N ∧ (∀ (c : E), c ∈ s → ‖c‖ ≤ 2) ∧ ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖}
refine' ⟨0, ⟨∅, by simp⟩⟩
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ Finset.card ∅ = 0 ∧ (∀ (c : E), c ∈ ∅ → ‖c‖ ≤ 2) ∧ ∀ (c : E), c ∈ ∅ → ∀ (d : E), d ∈ ∅ → c ≠ d → 1 ≤ ‖c - d‖
simp
case h₂.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
h : (∀ (c : E), c ∈ s → ‖c‖ ≤ 2) ∧ ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ ∀ (b : ℕ),
    b ∈
        {N |
          ∃ s,
            Finset.card s = N ∧
              (∀ (c : E), c ∈ s → ‖c‖ ≤ 2) ∧ ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖} →
      b ≤ 5 ^ finrank ℝ E
rintro _ ⟨s, ⟨rfl, h⟩⟩
no goals
case h₂.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
h : (∀ (c : E), c ∈ s → ‖c‖ ≤ 2) ∧ ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
exact Besicovitch.card_le_of_separated s h.1 h.2