lean_workbook_plus_60057
ProvedProve that where .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60057 (x y t : ℝ) (ht : t = x*y) : (x + y^2019) * (x^2019 + y) ≥ t * (t^1009 + 1)^2 := by sorry
Source
Prove that where .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_60057 (x y t : ℝ) (ht : t = x*y) : (x + y^2019) * (x^2019 + y) ≥ t * (t^1009 + 1)^2 := by sorry