theorem Circle.cos_eq_cos_of_exp_eq_exp {x y : ℝ} (h : exp x = exp y) : Real.cos x = Real.cos y

theorem Circle.sin_eq_sin_of_exp_eq_exp {x y : ℝ} (h : exp x = exp y) : Real.sin x = Real.sin y