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

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

x : ℝ
⊢ sin (π / 2 ^ 2) = sqrt 2 / 2
x : ℝ
⊢ sin (π / 4) = sin (π / 2 ^ 2)

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

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