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

State before:
m i : ℕ
⊢ invertible (F m i)
Tactic:
by_cases h : rel_prime m i
State after:
case pos
m i : ℕ
h : rel_prime m i
⊢ invertible (F m i)

case neg
m i : ℕ
h : ¬rel_prime m i
⊢ invertible (F m i)

State before:
case pos
m i : ℕ
h : rel_prime m i
⊢ invertible (F m i)
Tactic:
rewrite [F_rp_def h]
State after:
case pos
m i : ℕ
h : rel_prime m i
⊢ invertible [↑i]_m

State before:
case pos
m i : ℕ
h : rel_prime m i
⊢ invertible [↑i]_m
Tactic:
show invertible [i]_m from (Theorem_7_3_7 m i).rtl h
State after:
no goals

State before:
case neg
m i : ℕ
h : ¬rel_prime m i
⊢ invertible (F m i)
Tactic:
rewrite [F_not_rp_def h]
State after:
case neg
m i : ℕ
h : ¬rel_prime m i
⊢ invertible [1]_m

State before:
case neg
m i : ℕ
h : ¬rel_prime m i
⊢ invertible [1]_m
Tactic:
apply Exists.intro [1]_m
State after:
case neg
m i : ℕ
h : ¬rel_prime m i
⊢ [1]_m * [1]_m = [1]_m

State before:
case neg
m i : ℕ
h : ¬rel_prime m i
⊢ [1]_m * [1]_m = [1]_m
Tactic:
show [1]_m * [1]_m = [1]_m from Theorem_7_3_6_7 [1]_m
State after:
no goals