fix(tactic/norm_num): remove one_div from simp set (#4705)

fixes #4701

src/tactic/norm_num.lean

@@ -1420,7 +1420,7 @@ where `A` and `B` are numerical expressions.
 It also has a relatively simple primality prover. -/
 meta def norm_num (hs : parse simp_arg_list) (l : parse location) : tactic unit :=
 repeat1 $ orelse' (norm_num1 l) $
-simp_core {} (norm_num1 (loc.ns [none])) ff hs [] l
+simp_core {} (norm_num1 (loc.ns [none])) ff (simp_arg_type.except ``one_div :: hs) [] l
 
 add_hint_tactic "norm_num"
 
@@ -1487,6 +1487,7 @@ where `A` and `B` are numerical expressions.
 It also has a relatively simple primality prover. -/
 meta def norm_num (hs : parse simp_arg_list) : conv unit :=
 repeat1 $ orelse' norm_num1 $
-conv.interactive.simp ff hs [] { discharger := tactic.interactive.norm_num1 (loc.ns [none]) }
+conv.interactive.simp ff (simp_arg_type.except ``one_div :: hs) []
+  { discharger := tactic.interactive.norm_num1 (loc.ns [none]) }
 
 end conv.interactive

test/norm_num.lean

@@ -67,6 +67,13 @@ example (x : ℕ) : ℕ := begin
   exact n
 end
 
+example (a : ℚ) (h : 3⁻¹ * a = a) : true :=
+begin
+  norm_num at h,
+  guard_hyp h : 1 / 3 * a = a,
+  trivial
+end
+
 example : nat.prime 1277 := by norm_num
 example : nat.min_fac 221 = 13 := by norm_num