R : Type ?u.76609
E : Type ?u.76612
F : Type ?u.76615
ι : Type ?u.76618
ι' : Type ?u.76621
α : Type ?u.76624
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
f : ι → α
w : ι → R
hw₀ : ∀ (i : ι), i ∈ ∅ → 0 ≤ w i
hw₁ : 0 < ∑ i in ∅, w i
⊢ False
R : Type ?u.76609
E : Type ?u.76612
F : Type ?u.76615
ι : Type ?u.76618
ι' : Type ?u.76621
α : Type ?u.76624
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : 0 < ∑ i in s, w i
⊢ s ≠ ∅
rintro rfl
no goals
R : Type ?u.76609
E : Type ?u.76612
F : Type ?u.76615
ι : Type ?u.76618
ι' : Type ?u.76621
α : Type ?u.76624
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
f : ι → α
w : ι → R
hw₀ : ∀ (i : ι), i ∈ ∅ → 0 ≤ w i
hw₁ : 0 < ∑ i in ∅, w i
⊢ False
simp at hw₁