case pos
α : Type ?u.24169
M₀ : Type ?u.24172
G₀ : Type u_1
M₀' : Type ?u.24178
G₀' : Type ?u.24181
F : Type ?u.24184
F' : Type ?u.24187
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : a = 0
⊢ a * a * a⁻¹ = a

case neg
α : Type ?u.24169
M₀ : Type ?u.24172
G₀ : Type u_1
M₀' : Type ?u.24178
G₀' : Type ?u.24181
F : Type ?u.24184
F' : Type ?u.24187
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : ¬a = 0
⊢ a * a * a⁻¹ = a
α : Type ?u.24169
M₀ : Type ?u.24172
G₀ : Type u_1
M₀' : Type ?u.24178
G₀' : Type ?u.24181
F : Type ?u.24184
F' : Type ?u.24187
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a * a * a⁻¹ = a
by_cases h : a = 0
no goals
case pos
α : Type ?u.24169
M₀ : Type ?u.24172
G₀ : Type u_1
M₀' : Type ?u.24178
G₀' : Type ?u.24181
F : Type ?u.24184
F' : Type ?u.24187
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : a = 0
⊢ a * a * a⁻¹ = a
rw [h, inv_zero, mul_zero]
no goals
case neg
α : Type ?u.24169
M₀ : Type ?u.24172
G₀ : Type u_1
M₀' : Type ?u.24178
G₀' : Type ?u.24181
F : Type ?u.24184
F' : Type ?u.24187
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : ¬a = 0
⊢ a * a * a⁻¹ = a
rw [mul_assoc, mul_inv_cancel h, mul_one]