no goals
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : SemilatticeSup β
K : Set α
h₁ : IsComplete K
u : β → α
h₂ : ∀ (n : β), u n ∈ K
h₃ : CauchySeq u
⊢ u '' univ ⊆ K
rwa [image_univ, range_subset_iff]