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

State before:
m a i : ℕ
h1 : rel_prime m a
h2 : ¬rel_prime m i
⊢ F m (G m a i) = [1]_m
Tactic:
rewrite [←G_rp_iff h1 i] at h2
State after:
m a i : ℕ
h1 : rel_prime m a
h2 : ¬rel_prime m (G m a i)
⊢ F m (G m a i) = [1]_m

State before:
m a i : ℕ
h1 : rel_prime m a
h2 : ¬rel_prime m (G m a i)
⊢ F m (G m a i) = [1]_m
Tactic:
show F m (G m a i) = [1]_m from F_not_rp_def h2
State after:
no goals