Given a natural language math problem and its answer, please generate a corresponding Lean 4 formal statement.
Please add comments highlighting the original parts of the natural language math problem and answer.
Please explicitly use the variable `answer` to indicate the answer in the formal statement.
Please maintain the semantic equivalence between natural language math and Lean 4.
Please assume the following header code has already been executed and do not add any imports or openings.
```lean4
import Mathlib
open BigOperators Real Nat Topology

```

# Problem
"""
Given $2\sin (π-x)+1=0$, find the value of $\cos 2x$.
"""
# Answer
"""
the answer is \frac{1}{2}
"""

# Formal Statement
```lean4
example
(answer : ℝ)
  (x : ℝ)
  -- Given $2\sin (π-x)+1=0$
  (h_eq : 2 * Real.sin (Real.pi - x) + 1 = 0)
  -- Find the value of $\cos 2x$.
  (h_answer : Real.cos (2 * x) = answer)
: -- the answer is $\frac{1}{2}$
answer = 1/2
:= by
```

Given a natural language math problem, its answer, its solution, and its formal statement, please generate a corresponding Lean 4 proof sketch and add comments to highlight the original parts of the natural language math solution.
Please maintain the semantic equivalence between natural language math and Lean 4.
Please only use forward reasoning in the proof, do not use tactics that modify the final goal.
For new hypotheses, please do not prove them and use `sorry` to close them.
Please assume the following header code has already been executed and do not add any imports or openings.
```lean4
import Mathlib
```

# Problem
"""
Given $2\sin (π-x)+1=0$, find the value of $\cos 2x$.
"""
# Answer
"""
the answer is \frac{1}{2}
"""
# Solution
"""
The given equation can be simplified as follows:

$2\sin (π-x)+1=0$

Using the cofunction identity $\sin(π-x)=\sin(x)$, we have:

$2\sin(x)+1=0$

Now, solve for $\sin(x)$:

$\sin(x)=-\frac{1}{2}$

Now, we need to find $\cos 2x$. We can use the double angle identity for cosine:

$\cos 2x = 1 - 2\sin^2 x$

Substitute the value of $\sin x$:

$\cos 2x = 1 - 2(-\frac{1}{2})^2$

Simplify:

$\cos 2x = 1 - 2(\frac{1}{4})$

$\cos 2x = 1 - \frac{1}{2}$

$\cos 2x = \frac{1}{2}$

Thus, the value of $\cos 2x$ is $\boxed{\frac{1}{2}}$.
"""

# Formal Statement
```lean4
example
(answer : ℝ)
  (x : ℝ)
  -- Given $2\sin (π-x)+1=0$
  (h_eq : 2 * Real.sin (Real.pi - x) + 1 = 0)
  -- Find the value of $\cos 2x$.
  (h_answer : Real.cos (2 * x) = answer)
: -- the answer is $\frac{1}{2}$
answer = 1/2
:= by
```

# Formal Proof Draft
```lean4
-- The given equation can be simplified as follows: $2\sin (π-x)+1=0$
have h_given_eq : 2 * Real.sin (Real.pi - x) + 1 = 0 := h_eq

-- Using the cofunction identity $\sin(π-x)=\sin(x)$, we have: $2\sin(x)+1=0$
have h_cofunction : Real.sin (Real.pi - x) = Real.sin x := sorry
have h_simplified_eq : 2 * Real.sin x + 1 = 0 := sorry

-- Now, solve for $\sin(x)$: $\sin(x)=-\frac{1}{2}$
have h_sin_x : Real.sin x = -1/2 := sorry

-- Now, we need to find $\cos 2x$. We can use the double angle identity for cosine: $\cos 2x = 1 - 2\sin^2 x$
have h_double_angle : Real.cos (2 * x) = 1 - 2 * (Real.sin x)^2 := sorry

-- Substitute the value of $\sin x$: $\cos 2x = 1 - 2(-\frac{1}{2})^2$
have h_substituted : Real.cos (2 * x) = 1 - 2 * (-1/2)^2 := sorry

-- Simplify: $\cos 2x = 1 - 2(\frac{1}{4})$
have h_simplified : Real.cos (2 * x) = 1 - 2 * (1/4) := sorry

-- $\cos 2x = 1 - \frac{1}{2}$
have h_final_simplification : Real.cos (2 * x) = 1 - 1/2 := sorry

-- $\cos 2x = \frac{1}{2}$
have h_cos_2x : Real.cos (2 * x) = 1/2 := sorry

-- Thus, the value of $\cos 2x$ is $\boxed{\frac{1}{2}}$
have h_answer : answer = 1/2 := sorry

exact h_answer -- submit

```

Generate a tactic that can transform one step from the current tactic state to the 'no goals' tactic state.
Current tactic state:
```
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x y : L
m : ⨁ (i : ι), M i
⊢ ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
```

refine
  DFinsupp.ext fun _ =>
    ?_
      -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`

Given a natural language math problem and the current solution state, please generate the next solution step.
Please use comments to plan and reason in natural language and deductive reasoning to derive the answer.
Assume `Mathlib` is imported.
# Informal Problem
"""
Given $2\sin (π-x)+1=0$, find the value of $\cos 2x$.
"""
# Current Solution State
```lean4
case h.mp
answer x : ℝ
h_eq : 2 * Real.sin (Real.pi - x) + 1 = 0
h_answer : Real.cos (2 * x) = answer
h_given_eq : 2 * Real.sin (Real.pi - x) + 1 = 0
⊢ ?w
```

# Next Solution Step
```lean4
-- Using the cofunction identity $\sin(π-x)=\sin(x)$, we have: $2\sin(x)+1=0$
have h_cofunction : Real.sin (Real.pi - x) = Real.sin x := sorry
```