Theorem: HTPI.congr_mod_mod (HTPILib/Chap7.lean)

State before:
m : ℕ
a : ℤ
⊢ a ≡ a % ↑m (MOD m)
Tactic:
define
State after:
m : ℕ
a : ℤ
⊢ ∃ c, a - a % ↑m = ↑m * c

State before:
m : ℕ
a : ℤ
⊢ ∃ c, a - a % ↑m = ↑m * c
Tactic:
have h1 : m * (a / m) + a % m = a := Int.ediv_add_emod a m
State after:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ ∃ c, a - a % ↑m = ↑m * c

State before:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ ∃ c, a - a % ↑m = ↑m * c
Tactic:
apply Exists.intro (a / m)
State after:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ a - a % ↑m = ↑m * (a / ↑m)

State before:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ a - a % ↑m = ↑m * (a / ↑m)
Tactic:
show a - a % m = m * (a / m) from
  calc a - (a % m)
    _ = m * (a / m) + a % m - a % m := by rw [h1]
    _ = m * (a / m) := by ring
State after:
no goals

State before:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ a - a % ↑m = ↑m * (a / ↑m) + a % ↑m - a % ↑m
Tactic:
rw [h1]
State after:
no goals

State before:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ ↑m * (a / ↑m) + a % ↑m - a % ↑m = ↑m * (a / ↑m)
Tactic:
ring
State after:
no goals