no goals
ι : Type u
s : Finset ι
a b p q : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hpq : IsConjugateExponent p q
⊢ a * b ≤ a ^ p / p + b ^ q / q
simpa [← rpow_mul, ha, hb, hpq.ne_zero, hpq.symm.ne_zero, _root_.div_eq_inv_mul] using
  geom_mean_le_arith_mean2_weighted hpq.one_div_nonneg hpq.symm.one_div_nonneg
    (rpow_nonneg_of_nonneg ha p) (rpow_nonneg_of_nonneg hb q) hpq.inv_add_inv_conj