no goals
α : Type u_1
β : Type ?u.7335
A : Type ?u.7338
B : Type ?u.7341
M : Type u_2
N : Type ?u.7347
P : Type ?u.7350
R : Type ?u.7353
S : Type ?u.7356
G : Type ?u.7359
M₀ : Type ?u.7362
G₀ : Type ?u.7365
ι : Sort ?u.7368
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ Set.Nonempty (mulSupport f) ↔ f ≠ 1
rw [nonempty_iff_ne_empty, Ne.def, mulSupport_eq_empty_iff]