no goals
α : Type u_1
β : Type ?u.58789
γ : Type ?u.58792
ι : Type ?u.58795
M : Type u_2
M' : Type ?u.58801
N : Type ?u.58804
P : Type ?u.58807
G : Type ?u.58810
H : Type ?u.58813
R : Type ?u.58816
S : Type ?u.58819
inst✝ : Zero M
a a' : α
b : M
⊢ single a b = 0 ↔ b = 0
simp [FunLike.ext_iff, single_eq_set_indicator]