no goals
ι : Type u
s : Finset ι
w₁ w₂ p₁ p₂ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hw : w₁ + w₂ = 1
⊢ ↑({ val := w₁, property := hw₁ } + { val := w₂, property := hw₂ }) = ↑1
assumption