apply hxs
case refine_2.h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ ¬x i = 0 → i ∈ s
no goals