no goals
α : Type u_1
β : Type ?u.140404
γ : Type ?u.140407
ι : Type ?u.140410
M : Type u_2
M' : Type ?u.140416
N : Type ?u.140419
P : Type ?u.140422
G : Type ?u.140425
H : Type ?u.140428
R : Type ?u.140431
S : Type ?u.140434
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
⊢ ↑equivFunOnFinite.symm (Pi.single x m) = single x m
rw [← equivFunOnFinite_single, Equiv.symm_apply_apply]