case h
α : Type u_1
β : Type ?u.138459
γ : Type ?u.138462
ι : Type ?u.138465
M : Type u_2
M' : Type ?u.138471
N : Type ?u.138474
P : Type ?u.138477
G : Type ?u.138480
H : Type ?u.138483
R : Type ?u.138486
S : Type ?u.138489
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
x✝ : α
⊢ ↑equivFunOnFinite (single x m) x✝ = Pi.single x m x✝
α : Type u_1
β : Type ?u.138459
γ : Type ?u.138462
ι : Type ?u.138465
M : Type u_2
M' : Type ?u.138471
N : Type ?u.138474
P : Type ?u.138477
G : Type ?u.138480
H : Type ?u.138483
R : Type ?u.138486
S : Type ?u.138489
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
⊢ ↑equivFunOnFinite (single x m) = Pi.single x m
ext
no goals
case h
α : Type u_1
β : Type ?u.138459
γ : Type ?u.138462
ι : Type ?u.138465
M : Type u_2
M' : Type ?u.138471
N : Type ?u.138474
P : Type ?u.138477
G : Type ?u.138480
H : Type ?u.138483
R : Type ?u.138486
S : Type ?u.138489
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
x✝ : α
⊢ ↑equivFunOnFinite (single x m) x✝ = Pi.single x m x✝
simp [Finsupp.single_eq_pi_single, equivFunOnFinite]