no goals
α : Type u_1
β : Type ?u.2824
A : Type ?u.2827
B : Type ?u.2830
M : Type u_2
N : Type ?u.2836
P : Type ?u.2839
R : Type ?u.2842
S : Type ?u.2845
G : Type ?u.2848
M₀ : Type ?u.2851
G₀ : Type ?u.2854
ι : Sort ?u.2857
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
s : Set α
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s
simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', not_mem_compl_iff, EqOn,
  Pi.one_apply]