rw [mem_supportedFun_iff, support_subset_iff] at hx
case mk.a.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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ ¬x i = 0 → i ∈ s
case mk.a.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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
i : η
⊢ ¬x i = 0 → i ∈ s