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

State before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
⊢ a * inv_mod m a * i % m = i
Tactic:
have h3 : [a]_m * [inv_mod m a]_m = [1]_m := cc_mul_inv_mod_eq_one h1
State after:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : [↑a]_m * [↑(inv_mod m a)]_m = [1]_m
⊢ a * inv_mod m a * i % m = i

State before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : [↑a]_m * [↑(inv_mod m a)]_m = [1]_m
⊢ a * inv_mod m a * i % m = i
Tactic:
rewrite [mul_class, cc_eq_iff_congr, ←Nat.cast_mul, ←Nat.cast_one, congr_iff_mod_eq_Nat] at h3
State after:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : a * inv_mod m a % m = 1 % m
⊢ a * inv_mod m a * i % m = i

State before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : a * inv_mod m a % m = 1 % m
⊢ a * inv_mod m a * i % m = i
Tactic:
show a * inv_mod m a * i % m = i from
  calc a * (inv_mod m a) * i % m
    _ = (a * inv_mod m a) % m * i % m := by rw [mod_mul_mod_eq_mul_mod]
    _ = 1 % m * i % m := by rw [h3]
    _ = 1 * i % m := by rw [mod_mul_mod_eq_mul_mod]
    _ = i % m := by rw [one_mul]
    _ = i := Nat.mod_eq_of_lt h2
State after:
no goals

State before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : a * inv_mod m a % m = 1 % m
⊢ a * inv_mod m a * i % m = a * inv_mod m a % m * i % m
Tactic:
rw [mod_mul_mod_eq_mul_mod]
State after:
no goals

State before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : a * inv_mod m a % m = 1 % m
⊢ a * inv_mod m a % m * i % m = 1 % m * i % m
Tactic:
rw [h3]
State after:
no goals

State before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : a * inv_mod m a % m = 1 % m
⊢ 1 % m * i % m = 1 * i % m
Tactic:
rw [mod_mul_mod_eq_mul_mod]
State after:
no goals

State before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : a * inv_mod m a % m = 1 % m
⊢ 1 * i % m = i % m
Tactic:
rw [one_mul]
State after:
no goals