case inl
M : Type u_1
inst✝ : GroupWithZero M
ha : 0 ∈ center M
⊢ 0⁻¹ ∈ center M

case inr
M : Type u_1
inst✝ : GroupWithZero M
a : M
ha : a ∈ center M
ha0 : a ≠ 0
⊢ a⁻¹ ∈ center M
M : Type u_1
inst✝ : GroupWithZero M
a : M
ha : a ∈ center M
⊢ a⁻¹ ∈ center M
obtain rfl | ha0 := eq_or_ne a 0
case inr.intro
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : ↑a ∈ center M
ha0 : ↑a ≠ 0
⊢ (↑a)⁻¹ ∈ center M
case inr
M : Type u_1
inst✝ : GroupWithZero M
a : M
ha : a ∈ center M
ha0 : a ≠ 0
⊢ a⁻¹ ∈ center M
rcases IsUnit.mk0 _ ha0 with ⟨a, rfl⟩
case inr.intro
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : ↑a ∈ center M
ha0 : ↑a ≠ 0
⊢ ↑a⁻¹ ∈ center M
case inr.intro
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : ↑a ∈ center M
ha0 : ↑a ≠ 0
⊢ (↑a)⁻¹ ∈ center M
rw [← Units.val_inv_eq_inv_val]
no goals
case inr.intro
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : ↑a ∈ center M
ha0 : ↑a ≠ 0
⊢ ↑a⁻¹ ∈ center M
exact center_units_subset (inv_mem_center (subset_center_units ha))
case inl
M : Type u_1
inst✝ : GroupWithZero M
ha : 0 ∈ center M
⊢ 0 ∈ center M
case inl
M : Type u_1
inst✝ : GroupWithZero M
ha : 0 ∈ center M
⊢ 0⁻¹ ∈ center M
rw [inv_zero]
no goals
case inl
M : Type u_1
inst✝ : GroupWithZero M
ha : 0 ∈ center M
⊢ 0 ∈ center M
exact zero_mem_center M