simp (discharger := positivity) only [Real.log_mul, Real.log_rpow]
case h₁.h₂
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)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ (a ^ b * b ^ c * c ^ a).log ≤ (a ^ a * b ^ b * c ^ c).log
case h₁.h₂
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)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ b * a.log + c * b.log + a * c.log ≤ a * a.log + b * b.log + c * c.log