lean_workbook_plus_49682
Provedwhich is true for
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_49682 (t : ℝ) (ht : 2 ≤ t) : (7 - 2 * t) ^ 3 ≤ 3 * (t ^ 2 - 1) ^ 2 := by sorry
Source
which is true for
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_49682 (t : ℝ) (ht : 2 ≤ t) : (7 - 2 * t) ^ 3 ≤ 3 * (t ^ 2 - 1) ^ 2 := by sorry