lean_workbook_plus_30891
ProvedShow that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_30891 {x y : ℝ} : x ^ 4 + 6 * x ^ 2 * y ^ 2 + y ^ 4 ≥ 4 * x ^ 3 * y + 4 * x * y ^ 3 := by sorrySource
Show that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_30891 {x y : ℝ} : x ^ 4 + 6 * x ^ 2 * y ^ 2 + y ^ 4 ≥ 4 * x ^ 3 * y + 4 * x * y ^ 3 := by sorry