case pos
α : Type ?u.47
M₀ : Type u_1
G₀ : Type ?u.53
M₀' : Type ?u.56
G₀' : Type ?u.59
F : Type ?u.62
F' : Type ?u.65
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a

case neg
α : Type ?u.47
M₀ : Type u_1
G₀ : Type ?u.53
M₀' : Type ?u.56
G₀' : Type ?u.59
F : Type ?u.62
F' : Type ?u.65
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a
α : Type ?u.47
M₀ : Type u_1
G₀ : Type ?u.53
M₀' : Type ?u.56
G₀' : Type ?u.59
F : Type ?u.62
F' : Type ?u.65
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
⊢ inverse (a * b) = inverse b * inverse a
by_cases hab : IsUnit (a * b)
case neg.inl
α : Type ?u.47
M₀ : Type u_1
G₀ : Type ?u.53
M₀' : Type ?u.56
G₀' : Type ?u.59
F : Type ?u.62
F' : Type ?u.65
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
⊢ inverse (a * b) = inverse b * inverse a

case neg.inr
α : Type ?u.47
M₀ : Type u_1
G₀ : Type ?u.53
M₀' : Type ?u.56
G₀' : Type ?u.59
F : Type ?u.62
F' : Type ?u.65
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ inverse (a * b) = inverse b * inverse a
case neg
α : Type ?u.47
M₀ : Type u_1
G₀ : Type ?u.53
M₀' : Type ?u.56
G₀' : Type ?u.59
F : Type ?u.62
F' : Type ?u.65
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a
obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)
case pos.intro.intro.intro
α : Type ?u.47
M₀ : Type u_1
G₀ : Type ?u.53
M₀' : Type ?u.56
G₀' : Type ?u.59
F : Type ?u.62
F' : Type ?u.65
inst✝ : MonoidWithZero M₀
a b : M₀ˣ
h : Commute ↑a ↑b
hab : IsUnit (↑a * ↑b)
⊢ inverse (↑a * ↑b) = inverse ↑b * inverse ↑a
case pos
α : Type ?u.47
M₀ : Type u_1
G₀ : Type ?u.53
M₀' : Type ?u.56
G₀' : Type ?u.59
F : Type ?u.62
F' : Type ?u.65
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a
obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab
no goals
case pos.intro.intro.intro
α : Type ?u.47
M₀ : Type u_1
G₀ : Type ?u.53
M₀' : Type ?u.56
G₀' : Type ?u.59
F : Type ?u.62
F' : Type ?u.65
inst✝ : MonoidWithZero M₀
a b : M₀ˣ
h : Commute ↑a ↑b
hab : IsUnit (↑a * ↑b)
⊢ inverse (↑a * ↑b) = inverse ↑b * inverse ↑a
rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
no goals
case neg.inl
α : Type ?u.47
M₀ : Type u_1
G₀ : Type ?u.53
M₀' : Type ?u.56
G₀' : Type ?u.59
F : Type ?u.62
F' : Type ?u.65
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
⊢ inverse (a * b) = inverse b * inverse a
rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]
no goals
case neg.inr
α : Type ?u.47
M₀ : Type u_1
G₀ : Type ?u.53
M₀' : Type ?u.56
G₀' : Type ?u.59
F : Type ?u.62
F' : Type ?u.65
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ inverse (a * b) = inverse b * inverse a
rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]