α : Type ?u.15737
M₀ : Type ?u.15740
G₀ : Type u_1
M₀' : Type ?u.15746
G₀' : Type ?u.15749
F : Type ?u.15752
F' : Type ?u.15755
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
this : a * a⁻¹ = 1
⊢ False
α : Type ?u.15737
M₀ : Type ?u.15740
G₀ : Type u_1
M₀' : Type ?u.15746
G₀' : Type ?u.15749
F : Type ?u.15752
F' : Type ?u.15755
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
⊢ False
have := mul_inv_cancel h
no goals
α : Type ?u.15737
M₀ : Type ?u.15740
G₀ : Type u_1
M₀' : Type ?u.15746
G₀' : Type ?u.15749
F : Type ?u.15752
F' : Type ?u.15755
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
this : a * a⁻¹ = 1
⊢ False
simp [a_eq_0] at this