lean_workbook_plus_69161

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_69161 : ∀ a b c : ℝ, (a^2 * b + b^2 * c + c^2 * a) * (a * b / c + b * c / a + c * a / b)^2 ≥ (3 * a * b * c)^2 * (1 / a + 1 / b + 1 / c)   :=  by sorry