no goals
α : Type u_2
β : Type ?u.51375
γ : Type ?u.51378
ι : Type ?u.51381
M : Type u_1
M' : Type ?u.51387
N : Type ?u.51390
P : Type ?u.51393
G : Type ?u.51396
H : Type ?u.51399
R : Type ?u.51402
S : Type ?u.51405
inst✝ : Zero M
a✝ a' : α
b✝ : M
a x : α
b : M
⊢ ↑(single a b) x ≠ 0 ↔ x = a ∧ b ≠ 0
simp [single_apply_eq_zero]