simp [hc0 x hx]
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝¹ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
hc1 : ∀ (x : { x // x ∈ s }), c ↑x = g x
x : ι
x✝ : x ∈ Finset.univ
hx : x ∉ s
⊢ c x • f x = 0
no goals