simp only [Equiv.invFun_as_coe, Finsupp.equivFunOnFinite_symm_apply_support,
  Finite.toFinset_setOf, ne_eq, Finset.mem_univ, forall_true_left, not_not,
  Finsupp.equivFunOnFinite_symm_apply_toFun]
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ (Finsupp.equivFunOnFinite.invFun x).support, (Finsupp.equivFunOnFinite.invFun x) x_1 * w x_1 =
    ∑ i : η, x i * w i
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U V : Submodule R (η → R)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ Finset.filter (fun x_1 => ¬x x_1 = 0) Finset.univ, x x_1 * w x_1 = ∑ i : η, x i * w i