Prove2Me

lean_workbook_plus_67890

Proved

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

  ⟹  b−a=1,2  ⟹  ∣a−b∣≤2\implies b-a=1,2\implies \boxed{\boxed{\mid a-b\mid \le 2}}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_67890 (a b : ℝ) (h₁ : b - a = 1 ∨ b - a = 2) : |a - b| ≤ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph