no goals
α✝ : Type ?u.645884
M✝ : Type ?u.645887
N : Type ?u.645890
P : Type ?u.645893
R✝ : Type ?u.645896
S : Type ?u.645899
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
xy : α × β
⊢ ↑(↑(LinearEquiv.symm (finsuppProdLEquiv R)) f) xy = ↑(↑f xy.fst) xy.snd
conv_rhs =>
  rw [← (finsuppProdLEquiv R).apply_symm_apply f, finsuppProdLEquiv_apply, Prod.mk.eta]