no goals
α : Type u_2
β : Type ?u.49894
γ : Type ?u.49897
ι : Type ?u.49900
M : Type u_1
M' : Type ?u.49906
N : Type ?u.49909
P : Type ?u.49912
G : Type ?u.49915
H : Type ?u.49918
R : Type ?u.49921
S : Type ?u.49924
inst✝ : Zero M
a✝ a' : α
b✝ : M
a x : α
b : M
⊢ ↑(single a b) x = 0 ↔ x = a → b = 0
simp [single_eq_set_indicator]