ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
⊢ w i * z i = w i * x
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∑ i in s, w i * z i = ∑ i in s, w i * x
refine' sum_congr rfl fun i hi => _
case inl
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i = 0
⊢ w i * z i = w i * x

case inr
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i ≠ 0
⊢ w i * z i = w i * x
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
⊢ w i * z i = w i * x
cases' eq_or_ne (w i) 0 with hwi hwi
no goals
case inl
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i = 0
⊢ w i * z i = w i * x
rw [hwi, MulZeroClass.zero_mul, MulZeroClass.zero_mul]
no goals
case inr
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i ≠ 0
⊢ w i * z i = w i * x
rw [hx i hi hwi]
no goals
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∑ i in s, w i * x = x
rw [← sum_mul, hw', one_mul]