ext
case h.e'_4
α : 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
⊢ (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = a
case h.e'_4.h
α : 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✝ : ↑s
⊢ s.restrict (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x✝ = a x✝