no goals
α : Type u
β : Type v
γ : Type ?u.564674
δ : Type ?u.564677
ε : Type ?u.564680
ζ : Type ?u.564683
inst✝ : TopologicalSpace α
⊢ IsClosed (range down)
simp only [ULift.down_surjective.range_eq, isClosed_univ]