simp only [RelIso.coe_fn_toEquiv, orderIsoMapComap_apply, MapSubtype.relIso_apply, mem_map,
  coeSubtype, exists_exists_and_eq_and, LinearEquiv.ofInjective_apply, support_subset_iff,
  LinearMap.extendSubtype_eq_ite]
α : 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)
⊢ x ∈
      ↑((MapSubtype.relIso (LinearMap.range (LinearMap.extendSubtype R s)))
          ((orderIsoMapComap (LinearEquiv.ofInjective (LinearMap.extendSubtype R s) ⋯)).toEquiv U)) ↔
    support x ⊆ s ∧ s.restrict x ∈ U
α : 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