simp [h]
case intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ a * 1 + b * 1 = 1
no goals