lean_workbook_plus_36776

Proved

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

$a-b = \frac{(3x^2 + 7xy + 2y^2)-(2x^2 + 7xy + 3y^2)}{(2x+y)(3x+y)} = \frac{x^2 - y^2}{(2x+y)(3x+y)}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36776 (x y a b : ℝ) : a - b = (3 * x ^ 2 + 7 * x * y + 2 * y ^ 2 - (2 * x ^ 2 + 7 * x * y + 3 * y ^ 2)) / ((2 * x + y) * (3 * x + y)) → a - b = (x ^ 2 - y ^ 2) / ((2 * x + y) * (3 * x + y))   :=  by sorry

Source

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

View graph