no goals
α : Type u_1
β : Type ?u.132948
γ : Type ?u.132951
ι : Type ?u.132954
M : Type u_2
M' : Type ?u.132960
N : Type ?u.132963
P : Type ?u.132966
G : Type ?u.132969
H : Type ?u.132972
R : Type ?u.132975
S : Type ?u.132978
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Unique α
b' : M
⊢ single a b = single a' b' ↔ b = b'
rw [unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same, single_eq_same]