norm_num splits multiplication equality

Stream: general

[Yaël Dillies]

@Mario Carneiro, I just uncovered a minor bug in norm_num. It seems to apply docs#mul_eq_mul_right_iff under the hood, even though that's not in its specification:

import Mathlib.Tactic.NormNum

example (a b c : ℕ) : 4096 * a * c = 512 * 8 * b * c := by
  norm_num
-- Expected:
/-
unsolved goals
a b c : ℕ
⊢ 4096 * a * c = 4096 * b * c
-/
-- Actual:
/-
unsolved goals
a b c : ℕ
⊢ a = b ∨ c = 0
-/

[Eric Rodriguez]

It's a simp lemma, norm_num runs simp

[Eric Rodriguez]

norm_num1 won't