lean_workbook_plus_78970
OpenIf then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78970 (x y : ℝ) (h₁ : y = Real.sin (x + Real.pi / 4)) : Real.sin (2 * x) = 2 * y ^ 2 - 1 := by sorry
Source
If then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_78970 (x y : ℝ) (h₁ : y = Real.sin (x + Real.pi / 4)) : Real.sin (2 * x) = 2 * y ^ 2 - 1 := by sorry