ι : 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 : ι
hi : i ∈ s
⊢ z i ^ w i = x ^ w i
ι : 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, x ^ w i
refine' prod_congr rfl fun i hi => _
case inl
ι : 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 : ι
hi : i ∈ s
h₀ : w i = 0
⊢ z i ^ w i = x ^ w i

case inr
ι : 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 : ι
hi : i ∈ s
h₀ : w i ≠ 0
⊢ z i ^ w i = x ^ w i
ι : 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 : ι
hi : i ∈ s
⊢ z i ^ w i = x ^ w i
cases' eq_or_ne (w i) 0 with h₀ h₀
no goals
case inl
ι : 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 : ι
hi : i ∈ s
h₀ : w i = 0
⊢ z i ^ w i = x ^ w i
rw [h₀, rpow_zero, rpow_zero]
no goals
case inr
ι : 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 : ι
hi : i ∈ s
h₀ : w i ≠ 0
⊢ z i ^ w i = x ^ w i
rw [hx i hi h₀]
ι : 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
⊢ 0 ≤ x
ι : 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, x ^ w i = x
rw [← rpow_sum_of_nonneg _ hw, hw', rpow_one]
ι : 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
this : ∑ i in s, w i ≠ 0
⊢ 0 ≤ x
ι : 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
⊢ 0 ≤ x
have : (∑ i in s, w i) ≠ 0 := by
  rw [hw']
  exact one_ne_zero
case intro.intro
ι : 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
this : ∑ i in s, w i ≠ 0
i : ι
his : i ∈ s
hi : w i ≠ 0
⊢ 0 ≤ x
ι : 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
this : ∑ i in s, w i ≠ 0
⊢ 0 ≤ x
obtain ⟨i, his, hi⟩ := exists_ne_zero_of_sum_ne_zero this
case intro.intro
ι : 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
this : ∑ i in s, w i ≠ 0
i : ι
his : i ∈ s
hi : w i ≠ 0
⊢ 0 ≤ z i
case intro.intro
ι : 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
this : ∑ i in s, w i ≠ 0
i : ι
his : i ∈ s
hi : w i ≠ 0
⊢ 0 ≤ x
rw [← hx i his hi]
no goals
case intro.intro
ι : 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
this : ∑ i in s, w i ≠ 0
i : ι
his : i ∈ s
hi : w i ≠ 0
⊢ 0 ≤ z i
exact hz i his
ι : 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
⊢ 1 ≠ 0
ι : 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, w i ≠ 0
rw [hw']
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
⊢ 1 ≠ 0
exact one_ne_zero