no goals
R : Type u_2
E : Type u_1
F : Type ?u.69758
ι : Type u_3
ι' : Type ?u.69764
α : Type ?u.69767
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
i : ι
hit : i ∈ t
hit' : ¬i ∈ filter (fun i => w i ≠ 0) t
⊢ w i = 0
simpa only [hit, mem_filter, true_and_iff, Ne.def, Classical.not_not] using hit'