Theorem: Nat.mul_div_cancel (Runtime/Utilities/Std.lean)

State before:
m n : Nat
H : 0 < n
⊢ m * n / n = m
Tactic:
let t := add_mul_div_right 0 m H
State after:
m n : Nat
H : 0 < n
t : (0 + m * n) / n = 0 / n + m := add_mul_div_right 0 m H
⊢ m * n / n = m

State before:
m n : Nat
H : 0 < n
t : (0 + m * n) / n = 0 / n + m := add_mul_div_right 0 m H
⊢ m * n / n = m
Tactic:
rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t
State after:
no goals