Prove2Me

lean_workbook_plus_27297

Proved

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

(x−2)(x+1)2(x−3)<0⇔(x−2x−3<0,x+1≠0)⇔(2<x<3,x≠−1)⇔x∈(2,3)\frac{(x-2){{(x+1)}^{2}}}{(x-3)}<0\Leftrightarrow \left( \frac{x-2}{x-3}<0,x+1\ne 0 \right)\Leftrightarrow \left( 2<x<3,x\ne -1 \right)\Leftrightarrow x\in (2,3)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27297 (x : ℝ) (hx: x ≠ -1) (h : x ≠ 3): (x-2)*(x+1)^2/(x-3) < 0 ↔ 2 < x ∧ x < 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph