lean_workbook_plus_33551

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_33551 (x y z : ℝ) (hx: x > 0 ∧ y > 0 ∧ z > 0)(habc : x * y * z = 1) (h : x^2 + y^2 + z^2 = x * y * z + 4) :  ∃ a b c :ℝ, a > 0 ∧ b > 0 ∧ c > 0 ∧ a * b * c = 1 ∧ x = a + 1 / a ∧ y = b + 1 / b ∧ z = c + 1 / c   :=  by sorry