rw [eq_comm, Finset.sum_subset (Finset.subset_univ _)]
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ x : η, c x * y x = ∑ x ∈ c.support, c x * y x
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∀ x ∈ Finset.univ, x ∉ c.support → c x * y x = 0