no goals
α : Type u_1
β : Type ?u.31212
γ : Type ?u.31215
ι : Type ?u.31218
M : Type u_2
M' : Type ?u.31224
N : Type ?u.31227
P : Type ?u.31230
G : Type ?u.31233
H : Type ?u.31236
R : Type ?u.31239
S : Type ?u.31242
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ ↑(single a b) a' = if a = a' then b else 0
classical
simp_rw [@eq_comm _ a a']
convert Pi.single_apply a b a'
α : Type u_1
β : Type ?u.31212
γ : Type ?u.31215
ι : Type ?u.31218
M : Type u_2
M' : Type ?u.31224
N : Type ?u.31227
P : Type ?u.31230
G : Type ?u.31233
H : Type ?u.31236
R : Type ?u.31239
S : Type ?u.31242
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ ↑(single a b) a' = if a' = a then b else 0
α : Type u_1
β : Type ?u.31212
γ : Type ?u.31215
ι : Type ?u.31218
M : Type u_2
M' : Type ?u.31224
N : Type ?u.31227
P : Type ?u.31230
G : Type ?u.31233
H : Type ?u.31236
R : Type ?u.31239
S : Type ?u.31242
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ ↑(single a b) a' = if a = a' then b else 0
simp_rw [@eq_comm _ a a']
no goals
α : Type u_1
β : Type ?u.31212
γ : Type ?u.31215
ι : Type ?u.31218
M : Type u_2
M' : Type ?u.31224
N : Type ?u.31227
P : Type ?u.31230
G : Type ?u.31233
H : Type ?u.31236
R : Type ?u.31239
S : Type ?u.31242
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ ↑(single a b) a' = if a' = a then b else 0
convert Pi.single_apply a b a'