no goals
ι : Type u
s : Finset ι
w₁ w₂ p₁ p₂ : ℝ≥0
⊢ w₁ + w₂ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ ≤ w₁ * p₁ + w₂ * p₂
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
  Fintype.univ_of_isEmpty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one] using
  geom_mean_le_arith_mean_weighted univ ![w₁, w₂] ![p₁, p₂]