lean_workbook_plus_25423
OpenLHS from AM-GM \n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_25423 (x y : ℝ) : tan x ^ 4 + tan y ^ 4 ≥ 2 * tan x ^ 2 * tan y ^ 2 := by sorry
Source
LHS from AM-GM \n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_25423 (x y : ℝ) : tan x ^ 4 + tan y ^ 4 ≥ 2 * tan x ^ 2 * tan y ^ 2 := by sorry