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

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ [↑a]_m * [↑(inv_mod m a)]_m = [1]_m
Tactic:
have h2 : 0 ≤ (gcd_c2 m a) % m := mod_nonneg m (gcd_c2 m a)
State after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : 0 ≤ gcd_c2 m a % ↑m
⊢ [↑a]_m * [↑(inv_mod m a)]_m = [1]_m

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : 0 ≤ gcd_c2 m a % ↑m
⊢ [↑a]_m * [↑(inv_mod m a)]_m = [1]_m
Tactic:
show [a]_m * [inv_mod m a]_m = [1]_m from
  calc [a]_m * [inv_mod m a]_m
    _ = [a]_m * [Int.toNat ((gcd_c2 m a) % m)]_m := by rfl
    _ = [a]_m * [(gcd_c2 m a) % m]_m := by rw [Int.toNat_of_nonneg h2]
    _ = [a]_m * [gcd_c2 m a]_m := by rw [←cc_eq_mod]
    _ = [1]_m := gcd_c2_inv h1
State after:
no goals

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : 0 ≤ gcd_c2 m a % ↑m
⊢ [↑a]_m * [↑(inv_mod m a)]_m = [↑a]_m * [↑(Int.toNat (gcd_c2 m a % ↑m))]_m
Tactic:
rfl
State after:
no goals

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : 0 ≤ gcd_c2 m a % ↑m
⊢ [↑a]_m * [↑(Int.toNat (gcd_c2 m a % ↑m))]_m = [↑a]_m * [gcd_c2 m a % ↑m]_m
Tactic:
rw [Int.toNat_of_nonneg h2]
State after:
no goals

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : 0 ≤ gcd_c2 m a % ↑m
⊢ [↑a]_m * [gcd_c2 m a % ↑m]_m = [↑a]_m * [gcd_c2 m a]_m
Tactic:
rw [←cc_eq_mod]
State after:
no goals