diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index b3d89e07f747b..25a8dab03803f 100644
--- a/src/data/equiv/basic.lean
+++ b/src/data/equiv/basic.lean
@@ -633,12 +633,16 @@ protected noncomputable def image {α β} (f : α → β) (s : set α) (H : inje
 
 protected noncomputable def range {α β} (f : α → β) (H : injective f) :
   α ≃ range f :=
-(set.univ _).symm.trans $ (set.image f univ H).trans (equiv.cast $ by rw image_univ)
+{ to_fun := λ x, ⟨f x, mem_range_self _⟩,
+  inv_fun := λ x, classical.some x.2,
+  left_inv := λ x, H (classical.some_spec (show f x ∈ range f, from mem_range_self _)),
+  right_inv := λ x, subtype.eq $ classical.some_spec x.2 }
 
 @[simp] theorem range_apply {α β} (f : α → β) (H : injective f) (a) :
-  set.range f H a = ⟨f a, set.mem_range_self _⟩ :=
-by dunfold equiv.set.range equiv.set.univ;
-   simp [set_coe_cast, -image_univ, image_univ.symm]
+  set.range f H a = ⟨f a, set.mem_range_self _⟩ := rfl
+
+@[simp] theorem range_apply {α β} (f : α → β) (H : injective f) (a) :
+  set.range f H a = ⟨f a, set.mem_range_self _⟩ := rfl
 
 protected def congr {α β : Type*} (e : α ≃ β) : set α ≃ set β :=
 ⟨λ s, e '' s, λ t, e.symm '' t, symm_image_image e, symm_image_image e.symm⟩