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

State before:
m i : ℕ
h : ¬rel_prime m i
⊢ F m i = [1]_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 = [1]_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 = [1]_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 = [1]_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 = [1]_m
Tactic:
rewrite [h1, if_neg 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
⊢ [1]_m = [1]_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
⊢ [1]_m = [1]_m
Tactic:
rfl
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