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

State before:
m j : ℕ
h : ¬rel_prime m j
⊢ num_rp_below m (j + 1) = num_rp_below m j
Tactic:
have h1 : num_rp_below m (j +1) =
  if gcd m j = 1 then (num_rp_below m j) + 1
  else num_rp_below m j := by rfl
State after:
m j : ℕ
h : ¬rel_prime m j
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j

State before:
m j : ℕ
h : ¬rel_prime m j
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j
Tactic:
define at h
State after:
m j : ℕ
h : ¬gcd m j = 1
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j

State before:
m j : ℕ
h : ¬gcd m j = 1
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j
Tactic:
rewrite [if_neg h] at h1
State after:
m j : ℕ
h : ¬gcd m j = 1
h1 : num_rp_below m (j + 1) = num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j

State before:
m j : ℕ
h : ¬gcd m j = 1
h1 : num_rp_below m (j + 1) = num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j
Tactic:
show num_rp_below m (j + 1) = num_rp_below m j from h1
State after:
no goals

State before:
m j : ℕ
h : ¬rel_prime m j
⊢ num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
Tactic:
rfl
State after:
no goals