no goals
α : Type ?u.174230
β : Type u_2
γ : Type ?u.174236
δ : Type ?u.174239
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_1
ι : Type ?u.174254
f : κ → β
g : β → γ
hf : Surjective f
x : β
⊢ x ∈ closure (range f)
simp [hf.range_eq]