lean_workbook_plus_16558

Proved

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

If two linear expressions are equal for all values of $x$ , then their constants must be equal and the coefficients of the linear terms must be equal. In other words, if A, B, C, D are constants and

Ax + B = Cx + D

for all $x$ , then we must have $A = C$ and $B = D$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16558  (a b c d : ℝ)
  (h₀ : ∀ x, a * x + b = c * x + d) :
  a = c ∧ b = d   :=  by sorry

Source

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

View graph