calc 
  (message ^ public_key % (p * q)) ^ private_key % (p * q) 
    = (message ^ public_key) ^ private_key % (p * q)      := by rw [← Nat.pow_mod]
  _ = message ^ (public_key * private_key) % (p * q)      := by rw [pow_mul] 
  _ = message ^ (1 + (p - 1)*(q - 1)*k) % (p * q)         := by rw [hk]
  _ = message ^ (1 + totient (p*q)*k) % (p * q)           := by sorry 
  _ = (message * (message ^ totient (p * q))^k) % (p * q) := by rw [pow_add, pow_one, pow_mul]
  _ = (message % (p * q)) * ((message ^ totient (p * q))^k % (p * q)) % (p * q) 
                                                          := by rw [Nat.mul_mod]
  _ = (message % (p * q)) * 1 % (p * q)                   := by sorry 
  _ = message % (p * q)                                   := by rw [mul_one, Nat.mod_mod]
  _ = message                                             := by rw [Nat.mod_eq_of_lt h_msg]
case intro
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message
no goals