rfl
case neg
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
a_1 : α
ha_1 : a_1 ∈ x.support
hh : ¬f a_1 = f a
⊢ 0 = 0
no goals