Prove2Me

lean_workbook_plus_77449

Proved

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

Prove that f(x)=13+a×(12x+1−13)=a×12x+1+(1−a)13f(x)=\frac{1}{3}+a \times (\frac{1}{2x+1}-\frac{1}{3}) = a\times \frac{1}{2x+1} + (1-a) \frac{1}{3} for some constant aa.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77449 (f : ℝ → ℝ) (a : ℝ) (h₁ : ∀ x, f x = 1/3 + a * (1/(2*x + 1) - 1/3)) : ∀ x, f x = a * 1/(2*x + 1) + (1 - a) * 1/3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph