exact (Finsupp.mem_supported' _ _).1 l.2 _
case h.e'_3.h.a
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
i : ι
⊢ i ∉ s → ↑l i = 0
no goals