Prove2Me

lean_workbook_plus_68921

Proved

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

f(x) = x2−4x+3x2+x−6=(x−1)(x−3)(x−2)(x+3)\sqrt {\frac{{{x^2} - 4x + 3}}{{{x^2} + x - 6}}} = \sqrt {\frac{{(x - 1)(x - 3)}}{{(x - 2)(x + 3)}}}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68921  (x : ℝ)
  (h₀ : 0 < x)
  (h₁ : x ≠ 2)
  (h₂ : x ≠ -3)
  (h₃ : x^2 + x - 6 ≠ 0)
  (h₄ : x^2 - 4 * x + 3 ≥ 0) :
  Real.sqrt ((x^2 - 4 * x + 3) / (x^2 + x - 6)) = Real.sqrt ((x - 1) * (x - 3) / ((x - 2) * (x + 3)))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph