lean_workbook_plus_35569
ProvedThen we need to prove:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35569 (x z : ℝ) : x ^ 4 + z ^ 4 + 2 * x * z ^ 3 ≥ 2 * x ^ 3 * z + x ^ 2 * z ^ 2 := by sorry
Source
Then we need to prove:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_35569 (x z : ℝ) : x ^ 4 + z ^ 4 + 2 * x * z ^ 3 ≥ 2 * x ^ 3 * z + x ^ 2 * z ^ 2 := by sorry