no goals
α : Type ?u.14573
M₀ : Type ?u.14576
G₀ : Type u_1
M₀' : Type ?u.14582
G₀' : Type ?u.14585
F : Type ?u.14588
F' : Type ?u.14591
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b : G₀
p : (g : G₀) → g ≠ 0 → Prop
⊢ (∃ g hg, p g hg) ↔ ∃ g hg, p ↑(mk0 g hg) (_ : ↑(mk0 g hg) ≠ 0)
simp_rw [val_mk0]