lean_workbook_plus_44977
ProvedProve for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_44977 (t : ℝ) (ht : 0 < t ∧ t < 1) : (27 * t ^ 4 + 1) / (t ^ 2 - 2 * t + 1) ≥ 18 * t - 3 := by sorry
Source
Prove for .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_44977 (t : ℝ) (ht : 0 < t ∧ t < 1) : (27 * t ^ 4 + 1) / (t ^ 2 - 2 * t + 1) ≥ 18 * t - 3 := by sorry