lean_workbook_plus_24694

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If $|2b-1|\leq 1$ and $a(1-|2b-1|) =2b-1$ . Prove that $2b(1+|a|)=1+a+|a|$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24694 (a b : ℝ) (h₁ : |2 * b - 1| ≤ 1) (h₂ : a * (1 - |2 * b - 1|) = 2 * b - 1) : 2 * b * (1 + |a|) = 1 + a + |a|   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph