rw [eq]
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
⊢ (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
no goals