case pos
α : Type ?u.25133
M₀ : Type ?u.25136
G₀ : Type u_1
M₀' : Type ?u.25142
G₀' : Type ?u.25145
F : Type ?u.25148
F' : Type ?u.25151
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : a = 0
⊢ a⁻¹ * a * a = a

case neg
α : Type ?u.25133
M₀ : Type ?u.25136
G₀ : Type u_1
M₀' : Type ?u.25142
G₀' : Type ?u.25145
F : Type ?u.25148
F' : Type ?u.25151
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : ¬a = 0
⊢ a⁻¹ * a * a = a
α : Type ?u.25133
M₀ : Type ?u.25136
G₀ : Type u_1
M₀' : Type ?u.25142
G₀' : Type ?u.25145
F : Type ?u.25148
F' : Type ?u.25151
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a⁻¹ * a * a = a
by_cases h : a = 0
no goals
case pos
α : Type ?u.25133
M₀ : Type ?u.25136
G₀ : Type u_1
M₀' : Type ?u.25142
G₀' : Type ?u.25145
F : Type ?u.25148
F' : Type ?u.25151
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.25133
M₀ : Type ?u.25136
G₀ : Type u_1
M₀' : Type ?u.25142
G₀' : Type ?u.25145
F : Type ?u.25148
F' : Type ?u.25151
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : ¬a = 0
⊢ a⁻¹ * a * a = a
rw [inv_mul_cancel h, one_mul]