classical
obtain ⟨x, hx⟩ := x
rw [(s.supportedFunEquiv R).symm_apply_eq]
ext i
simp only [supportedFunEquiv_apply, LinearMap.extendSubtype_eq_ite, LinearMap.fun_Subtype_apply,
  dite_eq_ite]
rw [eq_comm, ite_eq_left_iff, not_imp_comm, eq_comm]
rw [mem_supportedFun_iff, support_subset_iff] at hx
apply hx
α : 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 : ↥(s.supportedFun R)
⊢ (s.supportedFunEquiv R).symm x = (LinearMap.funSubtype R s) ↑x
no goals