exact_mod_cast h
case a
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₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : v₁ a = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ ↑v₁.support ∪ ↑v₂.support
no goals