no goals
α : Type u_2
β : Type ?u.58510
γ : Type ?u.58513
ι : Type ?u.58516
M : Type u_1
M' : Type ?u.58522
N : Type ?u.58525
P : Type ?u.58528
G : Type ?u.58531
H : Type ?u.58534
R : Type ?u.58537
S : Type ?u.58540
inst✝ : Zero M
a a' : α
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ Disjoint (single i b).support (single j b').support ↔ i ≠ j
rw [support_single_ne_zero _ hb, support_single_ne_zero _ hb', disjoint_singleton]