Bolzano–Weierstrass theorem

import Mathlib

theorem bolzano_weierstrass {s : Set ℝ} (h : Bornology.IsBounded s) (hs : s.Infinite) : ∃ x, AccPt x (Filter.principal s) := by
  have hK_closed : IsClosed (closure s) := isClosed_closure
  have hK_bounded : Bornology.IsBounded (closure s) := Metric.isBounded_closure_of_isBounded h
  have hK_compact : IsCompact (closure s) := Metric.isCompact_iff_isClosed_bounded.2 ⟨hK_closed, hK_bounded⟩
  rcases hs.exists_accPt_of_subset_isCompact hK_compact subset_closure with ⟨x, _, hx⟩
  exact ⟨x, hx⟩