Theorem: HTPI.FG_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) = [↑a]_m * F m i
Tactic:
have h3 : rel_prime m (G m a i) := (G_rp_iff h1 i).rtl h2
State after:
m a i : ℕ
h1 : rel_prime m a
h2 : rel_prime m i
h3 : rel_prime m (G m a i)
⊢ F m (G m a i) = [↑a]_m * F m i

State before:
m a i : ℕ
h1 : rel_prime m a
h2 : rel_prime m i
h3 : rel_prime m (G m a i)
⊢ F m (G m a i) = [↑a]_m * F m i
Tactic:
show F m (G m a i) = [a]_m * F m i from
  calc F m (G m a i)
    _ = [G m a i]_m := F_rp_def h3
    _ = [a]_m * [i]_m := cc_G m a i
    _ = [a]_m * F m i := by rw [F_rp_def h2]
State after:
no goals

State before:
m a i : ℕ
h1 : rel_prime m a
h2 : rel_prime m i
h3 : rel_prime m (G m a i)
⊢ [↑a]_m * [↑i]_m = [↑a]_m * F m i
Tactic:
rw [F_rp_def h2]
State after:
no goals