ext
case h.refine_1.intro.intro.refine_1
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
⊢ ⇑((Finsupp.restrictSupportEquiv s K) l) = s.restrict ⇑↑l
case h.refine_1.intro.intro.refine_1.h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
x✝ : ↑s
⊢ ((Finsupp.restrictSupportEquiv s K) l) x✝ = s.restrict (⇑↑l) x✝