case inl
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : a ∈ center Mˣ
⊢ 0 * ↑a = ↑a * 0

case inr
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : a ∈ center Mˣ
b : M
hb : b ≠ 0
⊢ b * ↑a = ↑a * b
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : a ∈ center Mˣ
b : M
⊢ b * ↑a = ↑a * b
obtain rfl | hb := eq_or_ne b 0
no goals
case inl
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : a ∈ center Mˣ
⊢ 0 * ↑a = ↑a * 0
rw [zero_mul, mul_zero]
no goals
case inr
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : a ∈ center Mˣ
b : M
hb : b ≠ 0
⊢ b * ↑a = ↑a * b
exact Units.ext_iff.mp (ha (Units.mk0 _ hb))