Prove2Me

Simplifying a square-root coefficient

Proved
WorkbookSource.problem_21690

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

P(0,−12):f(0)=12⋅2f(−12)⇔2f(0)=22f(−12)\rm P(0,\dfrac{-1}{2}): f(0)=\dfrac{1}{\sqrt{2}}\cdot 2f(\dfrac{-1}{2})\Leftrightarrow 2f(0)=2\sqrt{2}f(\dfrac{-1}{2})

Source: InternLM Lean-Workbook, record lean_workbook_21690 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_21690 (f : ℝ → ℝ) (hf: f (0:ℝ) = 1 / Real.sqrt 2 * 2 * f (-1/2)) : 2 * f 0 = 2 * Real.sqrt 2 * f (-1/2)  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_21690; Apache-2.0

View graph