diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index dd5ea506b3..54afa3eeab 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -131,13 +131,30 @@ macro "max_prec" : term => `(1024)
 macro "default" : prio => `(prio| 1000)
 /-- The standardized "low" priority `low = 100`, for things that should be lower than default priority. -/
 macro "low"     : prio => `(prio| 100)
-/-- The standardized "medium" priority `med = 1000`. This is the same as `default`. -/
-macro "mid"     : prio => `(prio| 1000)
+/--
+The standardized "medium" priority `med = 1000`. This is lower than `default`, and higher than `low`.
+-/
+macro "mid"     : prio => `(prio| 500)
 /-- The standardized "high" priority `high = 10000`, for things that should be higher than default priority. -/
 macro "high"    : prio => `(prio| 10000)
 /-- Parentheses are used for grouping priority expressions. -/
 macro "(" p:prio ")" : prio => return p
 
+/-
+Note regarding priorities. We want `low < mid < default` because we have the following default instances:
+```
+@[default_instance low] instance (n : Nat) : OfNat Nat n where ...
+@[default_instance mid] instance : Neg Int where ...
+@[default_instance default] instance [Add α] : HAdd α α α where ...
+@[default_instance default] instance [Sub α] : HSub α α α where ...
+...
+```
+
+Monomorphic default instances must always "win" to preserve the Lean 3 monomorphic "look&feel".
+The `Neg Int` instance must have precedence over the `OfNat Nat n` one, otherwise we fail to elaborate `#check -42`
+See issue #1813 for an example that failed when `mid = default`.
+-/
+
 -- Basic notation for defining parsers
 -- NOTE: precedence must be at least `arg` to be used in `macro` without parentheses
 
diff --git a/tests/lean/1007.lean b/tests/lean/1007.lean
index 1f3c28d6f6..9e03b0d2b6 100644
--- a/tests/lean/1007.lean
+++ b/tests/lean/1007.lean
@@ -8,7 +8,7 @@ structure ℝ where
 instance instFoo1 {X : Type u} {Y : Type v} [Vec X] [Vec Y] : Vec (X × Y) := sorry
 instance instProblem {α : Type u} {X : Type v} [Vec X] : Vec (α → X) := sorry
 
-instance (priority := mid+1) instFoo2 : Vec ℝ := sorry
+instance (priority := default+1) instFoo2 : Vec ℝ := sorry
 
 --------------
 
diff --git a/tests/lean/1007.lean.expected.out b/tests/lean/1007.lean.expected.out
index 42f801dcf4..4b51f2095a 100644
--- a/tests/lean/1007.lean.expected.out
+++ b/tests/lean/1007.lean.expected.out
@@ -1,6 +1,6 @@
 1007.lean:8:9-8:17: warning: declaration uses 'sorry'
 1007.lean:9:9-9:20: warning: declaration uses 'sorry'
-1007.lean:11:29-11:37: warning: declaration uses 'sorry'
+1007.lean:11:33-11:41: warning: declaration uses 'sorry'
 1007.lean:15:9-15:20: warning: declaration uses 'sorry'
 1007.lean:34:0-34:8: warning: declaration uses 'sorry'
 1007.lean:35:0-35:8: warning: declaration uses 'sorry'
diff --git a/tests/lean/run/1813.lean b/tests/lean/run/1813.lean
new file mode 100644
index 0000000000..8b227509ed
--- /dev/null
+++ b/tests/lean/run/1813.lean
@@ -0,0 +1,4 @@
+example [Add α] [Neg α] [Mul α] [∀ n, OfNat α n] {a b : α} :=
+  calc
+    4 + 5 * b = -6 + 5 * (b + 2) := sorry
+            _ = -6 + 5 * 3 := sorry