no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
e : α ≃ β
he : UniformEmbedding ↑e
⊢ CompleteSpace α ↔ CompleteSpace β
rw [completeSpace_iff_isComplete_range he.toUniformInducing, e.range_eq_univ,
  completeSpace_iff_isComplete_univ]