lean_workbook_plus_4048

Proved

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

Expand and reduce the inequality to $\left(2a^{2}-c^{2}\right)^{2}+\left(2b^{2}-c^{2}\right)^{2}\geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4048 : ∀ a b c : ℝ, (2 * a ^ 2 - c ^ 2) ^ 2 + (2 * b ^ 2 - c ^ 2) ^ 2 ≥ 0   :=  by sorry

Source