rintro ⟨a, ha, rfl⟩
case refine_1
α : 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)
⊢ (∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x) → (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
case refine_1.intro.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 η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (∀ (x : η), (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x ≠ 0 → x ∈ s) ∧
    (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) ∈ U