simp only [mem_support, ne_eq, LinearMap.extendSubtype_eq_ite, dite_eq_right_iff,
  not_forall] at hi
case refine_1.intro
α : 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 η
y : ↑s → R
i : η
hi : i ∈ support ((LinearMap.extendSubtype R s) y)
⊢ i ∈ s
case refine_1.intro
α : 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 η
y : ↑s → R
i : η
hi : ∃ (x : i ∈ s), ¬y ⟨i, x⟩ = 0
⊢ i ∈ s