rintro ⟨y, rfl⟩ i hi
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
⊢ (∃ y, (LinearMap.extendSubtype R s) y = x) → support x ⊆ 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 : i ∈ support ((LinearMap.extendSubtype R s) y)
⊢ i ∈ s