x : ℝ
this : Real.sin x ^ 2 + Real.cos x ^ 2 = 1
⊢ ↑abs (cos ↑x + sin ↑x * I) = 1
x : ℝ
⊢ ↑abs (cos ↑x + sin ↑x * I) = 1
have := Real.sin_sq_add_cos_sq x
no goals
x : ℝ
this : Real.sin x ^ 2 + Real.cos x ^ 2 = 1
⊢ ↑abs (cos ↑x + sin ↑x * I) = 1
simp_all [add_comm, abs, normSq, sq, sin_ofReal_re, cos_ofReal_re, mul_re]