lean_workbook_plus_15715

Proved

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

case 1: $x=5$ \n $y+\sqrt{25-y^2}=7$ \n $25-y^2=(7-y)^2$ \n $2y^2-14y+24=0$ \n $y=4 ,y=3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15715  (x y : ℝ)
  (h₀ : x = 5)
  (h₁ : y + Real.sqrt (25 - y^2) = 7)
  (h₂ : 25 - y^2 = (7 - y)^2) :
  2 * y^2 - 14 * y + 24 = 0   :=  by sorry

Source

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

View graph