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

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

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
⊢ i < m → Ginv m a (G 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
⊢ Ginv m a (G m a i) = i

State before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ Ginv m a (G m a i) = i
Tactic:
show Ginv m a (G m a i) = i from
  calc Ginv m a (G m a i)
    _ = inv_mod m a * ((a * i) % m) % m := by rfl
    _ = inv_mod m a * (a * i) % m := by rw [mul_mod_mod_eq_mul_mod]
    _ = a * inv_mod m a * i % m := by rw [←mul_assoc, mul_comm (inv_mod m a)]
    _ = 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
⊢ Ginv m a (G m a i) = inv_mod m a * (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
⊢ inv_mod m a * (a * i % m) % m = inv_mod m a * (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
⊢ inv_mod m a * (a * i) % m = a * inv_mod m a * i % m
Tactic:
rw [←mul_assoc, mul_comm (inv_mod m a)]
State after:
no goals