no goals
α : Type ?u.16217
M₀ : Type ?u.16220
G₀ : Type u_1
M₀' : Type ?u.16226
G₀' : Type ?u.16229
F : Type ?u.16232
F' : Type ?u.16235
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a ≠ 0
⊢ a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹⁻¹
simp [inv_ne_zero h]
no goals
α : Type ?u.16217
M₀ : Type ?u.16220
G₀ : Type u_1
M₀' : Type ?u.16226
G₀' : Type ?u.16229
F : Type ?u.16232
F' : Type ?u.16235
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a ≠ 0
⊢ a⁻¹ * a * a⁻¹ * a⁻¹⁻¹ = a⁻¹ * a⁻¹⁻¹
simp [h]
no goals
α : Type ?u.16217
M₀ : Type ?u.16220
G₀ : Type u_1
M₀' : Type ?u.16226
G₀' : Type ?u.16229
F : Type ?u.16232
F' : Type ?u.16235
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a ≠ 0
⊢ a⁻¹ * a⁻¹⁻¹ = 1
simp [inv_ne_zero h]