case inl
α : Type ?u.20396
M₀ : Type ?u.20399
G₀ : Type u_1
M₀' : Type ?u.20405
G₀' : Type ?u.20408
F : Type ?u.20411
F' : Type ?u.20414
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
⊢ inverse 0 = 0⁻¹

case inr
α : Type ?u.20396
M₀ : Type ?u.20399
G₀ : Type u_1
M₀' : Type ?u.20405
G₀' : Type ?u.20408
F : Type ?u.20411
F' : Type ?u.20414
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
ha : a ≠ 0
⊢ inverse a = a⁻¹
α : Type ?u.20396
M₀ : Type ?u.20399
G₀ : Type u_1
M₀' : Type ?u.20405
G₀' : Type ?u.20408
F : Type ?u.20411
F' : Type ?u.20414
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ inverse a = a⁻¹
obtain rfl | ha := eq_or_ne a 0
no goals
case inl
α : Type ?u.20396
M₀ : Type ?u.20399
G₀ : Type u_1
M₀' : Type ?u.20405
G₀' : Type ?u.20408
F : Type ?u.20411
F' : Type ?u.20414
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
⊢ inverse 0 = 0⁻¹
simp
no goals
case inr
α : Type ?u.20396
M₀ : Type ?u.20399
G₀ : Type u_1
M₀' : Type ?u.20405
G₀' : Type ?u.20408
F : Type ?u.20411
F' : Type ?u.20414
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
ha : a ≠ 0
⊢ inverse a = a⁻¹
exact Ring.inverse_unit (Units.mk0 a ha)