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

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ ∀ i < m, G m a (Ginv m a i) = i
Tactic:
fix i : Nat
State after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
⊢ i < m → G m a (Ginv m a i) = i

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
⊢ i < m → G m a (Ginv m a i) = i
Tactic:
assume h2 : i < m
State after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ G m a (Ginv m a i) = i

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ G m a (Ginv m a i) = i
Tactic:
show G m a (Ginv m a i) = i from
  calc G m a (Ginv m a i)
    _ = a * ((inv_mod m a * i) % m) % m := by rfl
    _ = a * (inv_mod m a * i) % m := by rw [mul_mod_mod_eq_mul_mod]
    _ = a * inv_mod m a * i % m := by rw [←mul_assoc]
    _ = i := mul_inv_mod_cancel h1 h2
State after:
no goals

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ G m a (Ginv m a i) = a * (inv_mod m a * i % m) % m
Tactic:
rfl
State after:
no goals

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

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