have h1 : Nat.totient (p*q) = Nat.totient p * Nat.totient q := by
 rw [Nat.totient_mul hr]
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
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)