case h.h
ι : Type u_4
R✝ : Type ?u.89337
M : Type ?u.89340
η : ι → Type u_3
N : Type u_2
inst✝³ : Semiring R✝
R : Type u_1
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (r • f)) i✝) a✝ = ↑(↑(SMul.smul r (↑sigmaFinsuppEquivDfinsupp f)) i✝) a✝
ι : Type u_4
R✝ : Type ?u.89337
M : Type ?u.89340
η : ι → Type u_3
N : Type u_2
inst✝³ : Semiring R✝
R : Type u_1
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
⊢ ↑sigmaFinsuppEquivDfinsupp (r • f) = SMul.smul r (↑sigmaFinsuppEquivDfinsupp f)
ext
no goals
case h.h
ι : Type u_4
R✝ : Type ?u.89337
M : Type ?u.89340
η : ι → Type u_3
N : Type u_2
inst✝³ : Semiring R✝
R : Type u_1
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ↑(↑(↑sigmaFinsuppEquivDfinsupp (r • f)) i✝) a✝ = ↑(↑(SMul.smul r (↑sigmaFinsuppEquivDfinsupp f)) i✝) a✝
rfl