Theorem: Nat.mul_cancel_right (MLIR/Util/KDTensor.lean)

State before:
n m : ℕ
MODZERO : n % m = 0
⊢ n / m * m = n
Tactic:
rewrite [Nat.mod_zero_implies_div_mul_equal n m MODZERO]
State after:
n m : ℕ
MODZERO : n % m = 0
⊢ n = n

State before:
n m : ℕ
MODZERO : n % m = 0
⊢ n = n
Tactic:
rfl
State after:
no goals