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

State before:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n / modulus * modulus = n
Tactic:
have MULTIPLE: n = 0 + (n / modulus) * modulus := by {
  rewrite [<- MODZERO];
  rewrite [Nat.mul_comm];
  simp [Nat.mod_add_div];
}
State after:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = 0 + n / modulus * modulus
⊢ n / modulus * modulus = n

State before:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = 0 + n / modulus * modulus
⊢ n / modulus * modulus = n
Tactic:
simp at MULTIPLE
State after:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = n / modulus * modulus
⊢ n / modulus * modulus = n

State before:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = n / modulus * modulus
⊢ n / modulus * modulus = n
Tactic:
rewrite [<- MULTIPLE]
State after:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = n / modulus * modulus
⊢ n = n

State before:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = n / modulus * modulus
⊢ n = n
Tactic:
rfl
State after:
no goals

State before:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n = 0 + n / modulus * modulus
Tactic:
rewrite [<- MODZERO]
State after:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n = n % modulus + n / modulus * modulus

State before:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n = n % modulus + n / modulus * modulus
Tactic:
rewrite [Nat.mul_comm]
State after:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n = n % modulus + modulus * (n / modulus)

State before:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n = n % modulus + modulus * (n / modulus)
Tactic:
simp [Nat.mod_add_div]
State after:
no goals