x : ℝ
⊢ cos (π / 16) = cos (π / 2 ^ 4)

x : ℝ
⊢ cos (π / 2 ^ 4) = sqrt (2 + sqrt (2 + sqrt 2)) / 2
x : ℝ
⊢ cos (π / 16) = sqrt (2 + sqrt (2 + sqrt 2)) / 2
trans cos (π / 2 ^ 4)
case e_x.e_a
x : ℝ
⊢ 16 = 2 ^ 4

x : ℝ
⊢ cos (π / 2 ^ 4) = sqrt (2 + sqrt (2 + sqrt 2)) / 2
x : ℝ
⊢ cos (π / 16) = cos (π / 2 ^ 4)

x : ℝ
⊢ cos (π / 2 ^ 4) = sqrt (2 + sqrt (2 + sqrt 2)) / 2
congr
x : ℝ
⊢ cos (π / 2 ^ 4) = sqrt (2 + sqrt (2 + sqrt 2)) / 2
case e_x.e_a
x : ℝ
⊢ 16 = 2 ^ 4

x : ℝ
⊢ cos (π / 2 ^ 4) = sqrt (2 + sqrt (2 + sqrt 2)) / 2
norm_num
no goals
x : ℝ
⊢ cos (π / 2 ^ 4) = sqrt (2 + sqrt (2 + sqrt 2)) / 2
simp