[GOAL]
⊢ NoncompactSpace ℍ
[PROOFSTEP]
refine' ⟨fun h => _⟩
[GOAL]
h : IsCompact univ
⊢ False
[PROOFSTEP]
have : IsCompact (Complex.im ⁻¹' Ioi 0) := isCompact_iff_isCompact_univ.2 h
[GOAL]
h : IsCompact univ
this : IsCompact (Complex.im ⁻¹' Ioi 0)
⊢ False
[PROOFSTEP]
replace := this.isClosed.closure_eq
[GOAL]
h : IsCompact univ
this : closure (Complex.im ⁻¹' Ioi 0) = Complex.im ⁻¹' Ioi 0
⊢ False
[PROOFSTEP]
rw [closure_preimage_im, closure_Ioi, Set.ext_iff] at this 
[GOAL]
h : IsCompact univ
this : ∀ (x : ℂ), x ∈ Complex.im ⁻¹' Ici 0 ↔ x ∈ Complex.im ⁻¹' Ioi 0
⊢ False
[PROOFSTEP]
exact absurd ((this 0).1 (@left_mem_Ici ℝ _ 0)) (@lt_irrefl ℝ _ 0)
