no goals
α : Type ?u.15430
M₀ : Type ?u.15433
G₀ : Type u_1
M₀' : Type ?u.15439
G₀' : Type ?u.15442
F : Type ?u.15445
F' : Type ?u.15448
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b x : G₀
⊢ (∃ u, ↑u = x) ↔ x ≠ 0
simp [exists0]