case h₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ BddAbove
    {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
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ Finset.card s ∈
    {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‖}
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ Finset.card s ≤ multiplicity E
apply le_csSup
case h₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ 5 ^ finrank ℝ E ∈
    upperBounds
      {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
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ BddAbove
    {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' ⟨5 ^ finrank ℝ E, _⟩
case h₁.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s✝ : Finset E
hs : ∀ (c : E), c ∈ s✝ → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s✝ → ∀ (d : E), d ∈ s✝ → c ≠ d → 1 ≤ ‖c - d‖
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
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ 5 ^ finrank ℝ E ∈
    upperBounds
      {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‖}
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
hs : ∀ (c : E), c ∈ s✝ → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s✝ → ∀ (d : E), d ∈ s✝ → c ≠ d → 1 ≤ ‖c - d‖
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
case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ ∃ s_1,
    Finset.card s_1 = Finset.card s ∧
      (∀ (c : E), c ∈ s_1 → ‖c‖ ≤ 2) ∧ ∀ (c : E), c ∈ s_1 → ∀ (d : E), d ∈ s_1 → ¬c = d → 1 ≤ ‖c - d‖
case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ Finset.card s ∈
    {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‖}
simp only [mem_setOf_eq, Ne.def]
no goals
case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h's : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ ∃ s_1,
    Finset.card s_1 = Finset.card s ∧
      (∀ (c : E), c ∈ s_1 → ‖c‖ ≤ 2) ∧ ∀ (c : E), c ∈ s_1 → ∀ (d : E), d ∈ s_1 → ¬c = d → 1 ≤ ‖c - d‖
exact ⟨s, rfl, hs, h's⟩