apply le_of_pow_le_pow_left (by decide : 3 ≠ 0) (by positivity)
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ ((a * b * c) ^ ((a + b + c) / 3)) ^ 3 ≤ (a ^ a * b ^ b * c ^ c) ^ 3