diff --git a/library/data/real/division.lean b/library/data/real/division.lean
index 87f9af41fe..1d995d52c9 100644
--- a/library/data/real/division.lean
+++ b/library/data/real/division.lean
@@ -593,9 +593,11 @@ noncomputable definition real_has_inv [instance] [reducible] [priority real.prio
 noncomputable protected definition div (x y : ℝ) : ℝ :=
   x * y⁻¹
 
-noncomputable definition real_has_div [instance] [reducible] [priority real.prio] : has_div real :=
+noncomputable definition real_has_div : has_div real :=
   has_div.mk real.div
 
+local attribute real_has_div [instance] [reducible] [priority real.prio]
+
 protected theorem le_total (x y : ℝ) : x ≤ y ∨ y ≤ x :=
   quot.induction_on₂ x y (λ s t, rat_seq.r_le_total s t)