no goals
α : Type ?u.13598
M₀ : Type ?u.13601
G₀ : Type u_1
M₀' : Type ?u.13607
G₀' : Type ?u.13610
F : Type ?u.13613
F' : Type ?u.13616
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b✝ a b : G₀
ha : a ≠ 0
hb : b ≠ 0
h : mk0 a ha = mk0 b hb
⊢ a = b
injection h