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

State before:
m a : ℕ
h1 : rel_prime m a
i : ℕ
⊢ rel_prime m (G m a i) ↔ rel_prime m i
Tactic:
have h2 : invertible [a]_m := (Theorem_7_3_7 m a).rtl h1
State after:
m a : ℕ
h1 : rel_prime m a
i : ℕ
h2 : invertible [↑a]_m
⊢ rel_prime m (G m a i) ↔ rel_prime m i

State before:
m a : ℕ
h1 : rel_prime m a
i : ℕ
h2 : invertible [↑a]_m
⊢ rel_prime m (G m a i) ↔ rel_prime m i
Tactic:
show rel_prime m (G m a i) ↔ rel_prime m i from
  calc rel_prime m (G m a i)
    _ ↔ invertible [G m a i]_m := (Theorem_7_3_7 m (G m a i)).symm
    _ ↔ invertible ([a]_m * [i]_m) := by rw [cc_G]
    _ ↔ invertible [i]_m := prod_inv_iff_inv h2 ([i]_m)
    _ ↔ rel_prime m i := Theorem_7_3_7 m i
State after:
no goals

State before:
m a : ℕ
h1 : rel_prime m a
i : ℕ
h2 : invertible [↑a]_m
⊢ invertible [↑(G m a i)]_m ↔ invertible ([↑a]_m * [↑i]_m)
Tactic:
rw [cc_G]
State after:
no goals