case h.h
ι : Type u_3
R : Type ?u.76301
M : Type ?u.76304
η : ι → Type u_2
N : Type u_1
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (f + g)) i✝) a✝ =
    ↑(↑(↑sigmaFinsuppEquivDfinsupp f + ↑sigmaFinsuppEquivDfinsupp g) i✝) a✝
ι : Type u_3
R : Type ?u.76301
M : Type ?u.76304
η : ι → Type u_2
N : Type u_1
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
⊢ ↑sigmaFinsuppEquivDfinsupp (f + g) = ↑sigmaFinsuppEquivDfinsupp f + ↑sigmaFinsuppEquivDfinsupp g
ext
no goals
case h.h
ι : Type u_3
R : Type ?u.76301
M : Type ?u.76304
η : ι → Type u_2
N : Type u_1
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (f + g)) i✝) a✝ =
    ↑(↑(↑sigmaFinsuppEquivDfinsupp f + ↑sigmaFinsuppEquivDfinsupp g) i✝) a✝
rfl