natural mul_left

Stream: Is there code for X?

[Edison Xie]

import Mathlib

example (r n : ℕ) [NeZero n] [NeZero r] (hr1 : n = r * n) : r = 1 := by
  -- norm_num at hr1
  -- aesop
  -- simp at hr1
  simpa [mul_left_eq_self₀, NeZero.ne n] using hr1.symm

Is there a tactic that could solve this? Should there be one?

[Edison Xie]

cc @Yaël Dillies @Bhavik Mehta

[Kevin Buzzard]

It's not linear so omega doesn't work either

[Eric Wieser]

I don't think NeZero is supposed to be used in this case

[Andrew Yang]

We could add a variant of mul_left_eq_self₀ called eq_mul_left_self₀ and make it a simp lemma. I don't think one could ask for more.