ext i
case mk
α : 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 : η → R
hx : x ∈ s.supportedFun R
⊢ ⟨x, hx⟩ = (s.supportedFunEquiv R) ((LinearMap.funSubtype R s) ↑⟨x, hx⟩)
case mk.a.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 η
x✝ : η → R✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ ↑⟨x, hx⟩ i = ↑((s.supportedFunEquiv R) ((LinearMap.funSubtype R s) ↑⟨x, hx⟩)) i