[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
⊢ inverse (a * b) = inverse b * inverse a
[PROOFSTEP]
by_cases hab : IsUnit (a * b)
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a
[PROOFSTEP]
obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab
[GOAL]
case pos.intro.intro.intro
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀ˣ
h : Commute ↑a ↑b
hab : IsUnit (↑a * ↑b)
⊢ inverse (↑a * ↑b) = inverse ↑b * inverse ↑a
[PROOFSTEP]
rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a
[PROOFSTEP]
obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)
[GOAL]
case neg.inl
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
⊢ inverse (a * b) = inverse b * inverse a
[PROOFSTEP]
rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]
[GOAL]
case neg.inr
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ inverse (a * b) = inverse b * inverse a
[PROOFSTEP]
rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a / b) c
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b⁻¹) c
[PROOFSTEP]
exact hac.mul_left hbc.inv_left₀
