no goals
α : Type u_1
β : Type ?u.1849
A : Type ?u.1852
B : Type ?u.1855
M : Type u_2
N : Type ?u.1861
P : Type ?u.1864
R : Type ?u.1867
S : Type ?u.1870
G : Type ?u.1873
M₀ : Type ?u.1876
G₀ : Type ?u.1879
ι : Sort ?u.1882
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
s : Set α
⊢ mulSupport f = s ↔ (∀ (x : α), x ∈ s → f x ≠ 1) ∧ ∀ (x : α), ¬x ∈ s → f x = 1
simp (config := { contextual := true }) only [ext_iff, mem_mulSupport, ne_eq, iff_def,
  not_imp_comm, and_comm, forall_and]