Golfing the division of natural numbers

Stream: general

[Peiran Wu]

Is there a shorter proof for the following example? If not, would it be difficult to write a tactic that can prove things like this in one go? These are showing up a lot in a project I'm currently trying to refactor and golf. (I'm on v4.27.0.)

example (a b c : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : a * (b * c) / (b * a) = c := by
  ring_nf
  exact Nat.eq_div_of_mul_eq_right (Nat.mul_ne_zero ha hb) rfl |>.symm

[Ruben Van de Velde]

This also works:

import Mathlib

example (a b c : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : a * (b * c) / (b * a) = c :=
  Nat.div_eq_of_eq_mul_right (by positivity) (by ring_nf)

but generally I don't know of a good way to deal with those goals, no