simp only [Finsupp.restrictSupportEquiv, Equiv.coe_fn_mk, Finsupp.total_apply, Finsupp.sum,
  Finsupp.subtypeDomain_apply, smul_eq_mul]
case h.e'_2
α : 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
⊢ (Finsupp.total (↑s) K K y) ((Finsupp.restrictSupportEquiv s K) l) =
    (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l
case h.e'_2
α : 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
⊢ ∑ x ∈ (Finsupp.subtypeDomain (fun x => x ∈ s) ↑l).support, ↑l ↑x * y x =
    ∑ x ∈ (↑l).support, ↑l x * (LinearMap.extendSubtype K s) y x