no goals
A : Type u_2
B : Type u_1
inst✝¹ : DecidableEq A
inst✝ : One B
a : A
b b' : B
hb : b ≠ 1
hb' : b' ≠ 1
i j : A
⊢ Disjoint (mulSupport (mulSingle i b)) (mulSupport (mulSingle j b')) ↔ i ≠ j
rw [mulSupport_mulSingle_of_ne hb, mulSupport_mulSingle_of_ne hb', disjoint_singleton]