no goals
α : Type u_3
β : Type ?u.579469
γ : Type ?u.579472
ι : Type ?u.579475
M : Type u_1
M' : Type ?u.579481
N : Type ?u.579484
P : Type ?u.579487
G : Type ?u.579490
H : Type ?u.579493
R : Type u_2
S : Type ?u.579499
inst✝² : Zero M
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R M
a b : α
f : α → M
r : R
⊢ ↑(single a r) b • f a = ↑(single a (r • f b)) b
by_cases h : a = b <;> simp [h]