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

State before:
m i : ℕ
h : rel_prime m i
⊢ F m i = [↑i]_m
Tactic:
have h1 : F m i = if gcd m i = 1 then [i]_m else [1]_m := by rfl
State after:
m i : ℕ
h : rel_prime m i
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [↑i]_m

State before:
m i : ℕ
h : rel_prime m i
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [↑i]_m
Tactic:
define at h
State after:
m i : ℕ
h : gcd m i = 1
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [↑i]_m

State before:
m i : ℕ
h : gcd m i = 1
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [↑i]_m
Tactic:
rewrite [if_pos h] at h1
State after:
m i : ℕ
h : gcd m i = 1
h1 : F m i = [↑i]_m
⊢ F m i = [↑i]_m

State before:
m i : ℕ
h : gcd m i = 1
h1 : F m i = [↑i]_m
⊢ F m i = [↑i]_m
Tactic:
show F m i = [i]_m from h1
State after:
no goals

State before:
m i : ℕ
h : rel_prime m i
⊢ F m i = if gcd m i = 1 then [↑i]_m else [1]_m
Tactic:
rfl
State after:
no goals