lean_workbook_plus_69459
ProvedCase2:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69459 (a b c : ℝ) (hbc : b = c) : a^4 + 9 * a^2 * b^2 + 4 * b^4 ≥ 4 * a^3 * b + 10 * a * b^3 := by sorry
Source
Case2:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_69459 (a b c : ℝ) (hbc : b = c) : a^4 + 9 * a^2 * b^2 + 4 * b^4 ≥ 4 * a^3 * b + 10 * a * b^3 := by sorry