simp only [Finset.mem_univ, forall_true_left, not_not, Finset.mem_filter, true_and]
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.univ, x_1 ∉ Finset.filter (fun x_2 => ¬x x_2 = 0) Finset.univ → x x_1 * w x_1 = 0
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 : η), x x_1 = 0 → x x_1 * w x_1 = 0