no goals
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∏ i in s, z i ^ w i = ∑ i in s, w i * z i
rw [geom_mean_weighted_of_constant, arith_mean_weighted_of_constant] <;> assumption