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

State before:
p : ℕ
h1 : prime p
⊢ phi p = p - 1
Tactic:
have h2 : 1 ≤ p := prime_pos h1
State after:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
⊢ phi p = p - 1

State before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
⊢ phi p = p - 1
Tactic:
have h3 : p - 1 + 1 = p := Nat.sub_add_cancel h2
State after:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
⊢ phi p = p - 1

State before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
⊢ phi p = p - 1
Tactic:
have h4 : p - 1 < p := by linarith
State after:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
⊢ phi p = p - 1

State before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
⊢ phi p = p - 1
Tactic:
have h5 : num_rp_below p (p - 1 + 1) = p - 1 :=
  num_rp_prime h1 (p - 1) h4
State after:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
h5 : num_rp_below p (p - 1 + 1) = p - 1
⊢ phi p = p - 1

State before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
h5 : num_rp_below p (p - 1 + 1) = p - 1
⊢ phi p = p - 1
Tactic:
rewrite [h3] at h5
State after:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
h5 : num_rp_below p p = p - 1
⊢ phi p = p - 1

State before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
h4 : p - 1 < p
h5 : num_rp_below p p = p - 1
⊢ phi p = p - 1
Tactic:
show phi p = p - 1 from h5
State after:
no goals

State before:
p : ℕ
h1 : prime p
h2 : 1 ≤ p
h3 : p - 1 + 1 = p
⊢ p - 1 < p
Tactic:
linarith
State after:
no goals