no goals
α : Type u_3
β : Type ?u.86818
A : Type u_1
B : Type u_2
M : Type ?u.86827
N : Type ?u.86830
P : Type ?u.86833
R : Type ?u.86836
S : Type ?u.86839
G : Type ?u.86842
M₀ : Type ?u.86845
G₀ : Type ?u.86848
ι : Sort ?u.86851
inst✝² : AddMonoid A
inst✝¹ : Monoid B
inst✝ : DistribMulAction B A
b : B
f : α → A
x : α
hbf : x ∈ support (b • f)
hf : f x = 0
⊢ (b • f) x = 0
rw [Pi.smul_apply, hf, smul_zero]