obtain ⟨c, hc, rfl⟩ := h
case refine_1
α : 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, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x
y : η → R
hyU : y ∈ U
⊢ ∑ i : η, x i * y i = 0
case refine_1.intro.intro
α : 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
⊢ ∑ i : η, Finsupp.lcoeFun c i * y i = 0