conv_lhs =>
  congr; rfl; ext i
  rw [this i.1 i.2]
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
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : x a = 0
⊢ (∑ i : { x_1 // x_1 ∈ x.support }, if f ↑i = f a then x ↑i else 0) = x a
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
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : x a = 0
⊢ (∑ i : { x_1 // x_1 ∈ x.support }, if f ↑i = f a then x a else 0) = x a