A squared-distance bound under a quadratic relation

Proved

WorkbookSource.base_43092

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

$x^{2}-y^{2}=9-4y \implies d^{2}=x^{2}+y^{2}=2y^{2}-4y+9=2(y-1)^{2}+7 \geq 7$

Source: InternLM Lean-Workbook, record lean_workbook_43092 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_43092 (x y d : ℝ) (h₁ : x^2 - y^2 = 9 - 4*y) (h₂ : d^2 = x^2 + y^2): d^2 ≥ 7  :=  by sorry

Source