have h3 : Nat.totient (p*q) = (p - 1) * (q - 1) := by
 rw [h1, h2]
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)
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)