Homomorphism rules for Int used by the grind tactic. The natCast rules inject Nat operations into Int, shifts are normalized to arithmetic, and the %-cleanup rules remove redundant modular wrappers produced by injections into Int.

theorem Lean.Grind.Int.emod_mul_emod (m n k : Int) : m % n * k % n = m * k % n

theorem Lean.Grind.Int.mul_emod_emod (m n k : Int) : m * (n % k) % k = m * n % k