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

State before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
⊢ rel_prime a p
Tactic:
have h3 : gcd a p ∣ a := gcd_dvd_left a p
State after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
⊢ rel_prime a p

State before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
⊢ rel_prime a p
Tactic:
have h4 : gcd a p ∣ p := gcd_dvd_right a p
State after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
⊢ rel_prime a p

State before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
⊢ rel_prime a p
Tactic:
have h5 : gcd a p = 1 ∨ gcd a p = p := dvd_prime h1 h4
State after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
⊢ rel_prime a p

State before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
⊢ rel_prime a p
Tactic:
have h6 : gcd a p ≠ p := by
  contradict h2 with h6
  rewrite [h6] at h3
  show p ∣ a from h3
  done
State after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p ≠ p
⊢ rel_prime a p

State before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p ≠ p
⊢ rel_prime a p
Tactic:
disj_syll h5 h6
State after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h6 : gcd a p ≠ p
h5 : gcd a p = 1
⊢ rel_prime a p

State before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h6 : gcd a p ≠ p
h5 : gcd a p = 1
⊢ rel_prime a p
Tactic:
show rel_prime a p from h5
State after:
no goals

State before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
⊢ gcd a p ≠ p
Tactic:
contradict h2 with h6
State after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p = p
⊢ p ∣ a

State before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p = p
⊢ p ∣ a
Tactic:
rewrite [h6] at h3
State after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p = p
⊢ p ∣ a

State before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p = p
⊢ p ∣ a
Tactic:
show p ∣ a from h3
State after:
no goals