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

State before:
m a : ℕ
h1 : rel_prime m a
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Tactic:
set s : Int := gcd_c1 m a
State after:
m a : ℕ
h1 : rel_prime m a
s : ℤ := gcd_c1 m a
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m

State before:
m a : ℕ
h1 : rel_prime m a
s : ℤ := gcd_c1 m a
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Tactic:
have h2 : s * m + (gcd_c2 m a) * a = gcd m a := gcd_lin_comb a m
State after:
m a : ℕ
h1 : rel_prime m a
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = ↑(gcd m a)
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m

State before:
m a : ℕ
h1 : rel_prime m a
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = ↑(gcd m a)
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Tactic:
define at h1
State after:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = ↑(gcd m a)
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m

State before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = ↑(gcd m a)
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Tactic:
rewrite [h1, Nat.cast_one] at h2
State after:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m

State before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Tactic:
rewrite [mul_class, cc_eq_iff_congr]
State after:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ↑a * gcd_c2 m a ≡ 1 (MOD m)

State before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ↑a * gcd_c2 m a ≡ 1 (MOD m)
Tactic:
define
State after:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ∃ c, ↑a * gcd_c2 m a - 1 = ↑m * c

State before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ∃ c, ↑a * gcd_c2 m a - 1 = ↑m * c
Tactic:
apply Exists.intro (-s)
State after:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ↑a * gcd_c2 m a - 1 = ↑m * -s

State before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ↑a * gcd_c2 m a - 1 = ↑m * -s
Tactic:
show a * (gcd_c2 m a) - 1 = m * (-s) from
  calc a * (gcd_c2 m a) - 1
    _ = s * m + (gcd_c2 m a) * a + m * (-s) - 1 := by ring
    _ = 1 + m * (-s) - 1 := by rw [h2]
    _ = m * (-s) := by ring
State after:
no goals

State before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ↑a * gcd_c2 m a - 1 = s * ↑m + gcd_c2 m a * ↑a + ↑m * -s - 1
Tactic:
ring
State after:
no goals

State before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ s * ↑m + gcd_c2 m a * ↑a + ↑m * -s - 1 = 1 + ↑m * -s - 1
Tactic:
rw [h2]
State after:
no goals

State before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ 1 + ↑m * -s - 1 = ↑m * -s
Tactic:
ring
State after:
no goals