Theorem: totient_product_of_two_primes (RSAProject/rsaproject.lean)

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Tactic:
have h1 : Nat.totient (p*q) = Nat.totient p * Nat.totient q := by
 rw [Nat.totient_mul hr]
State after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Tactic:
have h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1) := by
 rw [totient_of_prime p hp, totient_of_prime q hq]
State after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Tactic:
have h3 : Nat.totient (p*q) = (p - 1) * (q - 1) := by
 rw [h1, h2]
State after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
h3 : Nat.totient (p * q) = (p - 1) * (q - 1)
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
h3 : Nat.totient (p * q) = (p - 1) * (q - 1)
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Tactic:
apply h3
State after:
no goals

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
⊢ Nat.totient (p * q) = Nat.totient p * Nat.totient q
Tactic:
rw [Nat.totient_mul hr]
State after:
no goals

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
⊢ Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
Tactic:
rw [totient_of_prime p hp, totient_of_prime q hq]
State after:
no goals

State before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Tactic:
rw [h1, h2]
State after:
no goals