no goals
α✝ : Type ?u.639667
M✝ : Type ?u.639670
N : Type ?u.639673
P : Type ?u.639676
R✝ : Type ?u.639679
S : Type ?u.639682
inst✝¹⁰ : Semiring R✝
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R✝ N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R✝ P
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α × β →₀ M
x : α
y : β
⊢ ↑(↑(↑(finsuppProdLEquiv R) f) x) y = ↑f (x, y)
rw [finsuppProdLEquiv, LinearEquiv.coe_mk, finsuppProdEquiv, Finsupp.curry_apply]