no goals
α : Type u
β : Type v
ι : Type ?u.162597
π : ι → Type ?u.162602
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
e : β → α
he : ClosedEmbedding e
⊢ (⋃ (n : ℕ), (fun n => e ⁻¹' compactCovering α n) n) = univ
rw [← preimage_iUnion, iUnion_compactCovering, preimage_univ]