x : ℝ
⊢ sin (π / 8) = sin (π / 2 ^ 3)

x : ℝ
⊢ sin (π / 2 ^ 3) = sqrt (2 - sqrt 2) / 2
x : ℝ
⊢ sin (π / 8) = sqrt (2 - sqrt 2) / 2
trans sin (π / 2 ^ 3)
case e_x.e_a
x : ℝ
⊢ 8 = 2 ^ 3

x : ℝ
⊢ sin (π / 2 ^ 3) = sqrt (2 - sqrt 2) / 2
x : ℝ
⊢ sin (π / 8) = sin (π / 2 ^ 3)

x : ℝ
⊢ sin (π / 2 ^ 3) = sqrt (2 - sqrt 2) / 2
congr
x : ℝ
⊢ sin (π / 2 ^ 3) = sqrt (2 - sqrt 2) / 2
case e_x.e_a
x : ℝ
⊢ 8 = 2 ^ 3

x : ℝ
⊢ sin (π / 2 ^ 3) = sqrt (2 - sqrt 2) / 2
norm_num
no goals
x : ℝ
⊢ sin (π / 2 ^ 3) = sqrt (2 - sqrt 2) / 2
simp