no goals
α : Type u_1
β : Type u_3
γ : Type ?u.168671
ι : Type ?u.168674
M : Type u_2
M' : Type ?u.168680
N : Type ?u.168683
P : Type ?u.168686
G : Type ?u.168689
H✝ : Type ?u.168692
R : Type ?u.168695
S : Type ?u.168698
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f g : α → β
h : ∀ (x : α), x ∈ v.support → f x = g x
x✝ : α
H : x✝ ∈ v.support
⊢ (fun a => single (f a)) x✝ (↑v x✝) = (fun a => single (g a)) x✝ (↑v x✝)
simp only [h _ H]