Prove2Me

lean_workbook_plus_6400

Proved

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

(3pq−1)=a(pq−p−q+1)==>(a−3)pq+a+1=a(p+q)(3pq-1)=a(pq-p-q+1) ==> (a-3)pq+a+1=a(p+q)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6400  (p q a : ℂ)
  (h₀ : (3 * p * q - 1) = a * (p * q - p - q + 1)) :
  (a - 3) * p * q + a + 1 = a * (p + q)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph