Commuting pairs of elements in monoids

We define the predicate Commute a b := a * b = b * a and provide some operations on terms (h : Commute a b). E.g., if a, b, and c are elements of a semiring, and that hb : Commute a b and hc : Commute a c. Then hb.pow_left 5 proves Commute (a ^ 5) b and (hb.pow_right 2).add_right (hb.mul_right hc) proves Commute a (b ^ 2 + b * c).

Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like rw [(hb.pow_left 5).eq] rather than just rw [hb.pow_left 5].

This file defines only a few operations (mul_left, inv_right, etc). Other operations (pow_right, field inverse etc) are in the files that define corresponding notions.

Implementation details

Most of the proofs come from the properties of SemiconjBy.

ink

def AddCommute {S : Type u_1} [inst : Add S] (a : S) (b : S) : Prop

Two elements additively commute if a + b = b + a

Equations

• AddCommute a b = AddSemiconjBy a b b

ink

def Commute {S : Type u_1} [inst : Mul S] (a : S) (b : S) : Prop

Two elements commute if a * b = b * a.

Equations

• Commute a b = SemiconjBy a b b

ink

theorem AddCommute.eq {S : Type u_1} [inst : Add S] {a : S} {b : S} (h : AddCommute a b) : a + b = b + a

Equality behind add_commute a b; useful for rewriting.

ink

theorem Commute.eq {S : Type u_1} [inst : Mul S] {a : S} {b : S} (h : Commute a b) : a * b = b * a

Equality behind Commute a b; useful for rewriting.

ink

@[simp]

theorem AddCommute.refl {S : Type u_1} [inst : Add S] (a : S) : AddCommute a a

Any element commutes with itself.

ink

@[simp]

theorem Commute.refl {S : Type u_1} [inst : Mul S] (a : S) : Commute a a

Any element commutes with itself.

ink

theorem AddCommute.symm {S : Type u_1} [inst : Add S] {a : S} {b : S} (h : AddCommute a b) : AddCommute b a

If a commutes with b, then b commutes with a.

ink

theorem Commute.symm {S : Type u_1} [inst : Mul S] {a : S} {b : S} (h : Commute a b) : Commute b a

If a commutes with b, then b commutes with a.

ink

theorem AddCommute.semiconjBy {S : Type u_1} [inst : Add S] {a : S} {b : S} (h : AddCommute a b) : AddSemiconjBy a b b

ink

theorem Commute.semiconjBy {S : Type u_1} [inst : Mul S] {a : S} {b : S} (h : Commute a b) : SemiconjBy a b b

ink

theorem AddCommute.symm_iff {S : Type u_1} [inst : Add S] {a : S} {b : S} : AddCommute a b ↔ AddCommute b a

ink

theorem Commute.symm_iff {S : Type u_1} [inst : Mul S] {a : S} {b : S} : Commute a b ↔ Commute b a

ink

instance AddCommute.instIsReflCommute {S : Type u_1} [inst : Add S] : IsRefl S AddCommute

Equations

• @AddCommute.instIsReflCommute = @AddCommute.instIsReflCommute.proof_1

ink

def AddCommute.instIsReflCommute.proof_1 {S : Type u_1} [inst : Add S] : IsRefl S AddCommute

Equations

• (_ : IsRefl S AddCommute) = (_ : IsRefl S AddCommute)

ink

instance Commute.instIsReflCommute {S : Type u_1} [inst : Mul S] : IsRefl S Commute

Equations

• @Commute.instIsReflCommute = @Commute.instIsReflCommute.proof_1

ink

instance AddCommute.on_isRefl {G : Type u_1} {S : Type u_2} [inst : Add S] {f : G → S} : IsRefl G fun a b => AddCommute (f a) (f b)

Equations

• @AddCommute.on_isRefl = @AddCommute.on_isRefl.proof_1

ink

def AddCommute.on_isRefl.proof_1 {G : Type u_1} {S : Type u_2} [inst : Add S] {f : G → S} : IsRefl G fun a b => AddCommute (f a) (f b)

Equations

• (_ : IsRefl G fun a b => AddCommute (f a) (f b)) = (_ : IsRefl G fun a b => AddCommute (f a) (f b))

ink

instance Commute.on_isRefl {G : Type u_1} {S : Type u_2} [inst : Mul S] {f : G → S} : IsRefl G fun a b => Commute (f a) (f b)

Equations

• @Commute.on_isRefl = @Commute.on_isRefl.proof_1

ink

@[simp]

theorem AddCommute.add_right {S : Type u_1} [inst : AddSemigroup S] {a : S} {b : S} {c : S} (hab : AddCommute a b) (hac : AddCommute a c) : AddCommute a (b + c)

If a commutes with both b and c, then it commutes with their sum.

ink

@[simp]

theorem Commute.mul_right {S : Type u_1} [inst : Semigroup S] {a : S} {b : S} {c : S} (hab : Commute a b) (hac : Commute a c) : Commute a (b * c)

If a commutes with both b and c, then it commutes with their product.

ink

@[simp]

theorem AddCommute.add_left {S : Type u_1} [inst : AddSemigroup S] {a : S} {b : S} {c : S} (hac : AddCommute a c) (hbc : AddCommute b c) : AddCommute (a + b) c

If both a and b commute with c, then their product commutes with c.

ink

@[simp]

theorem Commute.mul_left {S : Type u_1} [inst : Semigroup S] {a : S} {b : S} {c : S} (hac : Commute a c) (hbc : Commute b c) : Commute (a * b) c

If both a and b commute with c, then their product commutes with c.

ink

theorem AddCommute.right_comm {S : Type u_1} [inst : AddSemigroup S] {b : S} {c : S} (h : AddCommute b c) (a : S) : a + b + c = a + c + b

ink

theorem Commute.right_comm {S : Type u_1} [inst : Semigroup S] {b : S} {c : S} (h : Commute b c) (a : S) : a * b * c = a * c * b

ink

theorem AddCommute.left_comm {S : Type u_1} [inst : AddSemigroup S] {a : S} {b : S} (h : AddCommute a b) (c : S) : a + (b + c) = b + (a + c)

ink

theorem Commute.left_comm {S : Type u_1} [inst : Semigroup S] {a : S} {b : S} (h : Commute a b) (c : S) : a * (b * c) = b * (a * c)

ink

theorem AddCommute.add_add_add_comm {S : Type u_1} [inst : AddSemigroup S] {b : S} {c : S} (hbc : AddCommute b c) (a : S) (d : S) : a + b + (c + d) = a + c + (b + d)

ink

theorem Commute.mul_mul_mul_comm {S : Type u_1} [inst : Semigroup S] {b : S} {c : S} (hbc : Commute b c) (a : S) (d : S) : a * b * (c * d) = a * c * (b * d)

ink

theorem AddCommute.all {S : Type u_1} [inst : AddCommSemigroup S] (a : S) (b : S) : AddCommute a b

ink

theorem Commute.all {S : Type u_1} [inst : CommSemigroup S] (a : S) (b : S) : Commute a b

ink

@[simp]

theorem AddCommute.zero_right {M : Type u_1} [inst : AddZeroClass M] (a : M) : AddCommute a 0

ink

@[simp]

theorem Commute.one_right {M : Type u_1} [inst : MulOneClass M] (a : M) : Commute a 1

ink

@[simp]

theorem AddCommute.zero_left {M : Type u_1} [inst : AddZeroClass M] (a : M) : AddCommute 0 a

ink

@[simp]

theorem Commute.one_left {M : Type u_1} [inst : MulOneClass M] (a : M) : Commute 1 a

ink

@[simp]

theorem AddCommute.nsmul_right {M : Type u_1} [inst : AddMonoid M] {a : M} {b : M} (h : AddCommute a b) (n : ℕ) : AddCommute a (n • b)

ink

@[simp]

theorem Commute.pow_right {M : Type u_1} [inst : Monoid M] {a : M} {b : M} (h : Commute a b) (n : ℕ) : Commute a (b ^ n)

ink

@[simp]

theorem AddCommute.nsmul_left {M : Type u_1} [inst : AddMonoid M] {a : M} {b : M} (h : AddCommute a b) (n : ℕ) : AddCommute (n • a) b

ink

@[simp]

theorem Commute.pow_left {M : Type u_1} [inst : Monoid M] {a : M} {b : M} (h : Commute a b) (n : ℕ) : Commute (a ^ n) b

ink

@[simp]

theorem AddCommute.nsmul_nsmul {M : Type u_1} [inst : AddMonoid M] {a : M} {b : M} (h : AddCommute a b) (m : ℕ) (n : ℕ) : AddCommute (m • a) (n • b)

ink

@[simp]

theorem Commute.pow_pow {M : Type u_1} [inst : Monoid M] {a : M} {b : M} (h : Commute a b) (m : ℕ) (n : ℕ) : Commute (a ^ m) (b ^ n)

ink

theorem AddCommute.self_nsmul {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ) : AddCommute a (n • a)

ink

theorem Commute.self_pow {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ) : Commute a (a ^ n)

ink

theorem AddCommute.nsmul_self {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ) : AddCommute (n • a) a

ink

theorem Commute.pow_self {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ) : Commute (a ^ n) a

ink

theorem AddCommute.nsmul_nsmul_self {M : Type u_1} [inst : AddMonoid M] (a : M) (m : ℕ) (n : ℕ) : AddCommute (m • a) (n • a)

ink

theorem Commute.pow_pow_self {M : Type u_1} [inst : Monoid M] (a : M) (m : ℕ) (n : ℕ) : Commute (a ^ m) (a ^ n)

ink

theorem succ_nsmul' {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ) : (n + 1) • a = n • a + a

ink

theorem pow_succ' {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ) : a ^ (n + 1) = a ^ n * a

ink

theorem AddCommute.addUnits_neg_right {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M} : AddCommute a ↑u → AddCommute a ↑(-u)

ink

theorem Commute.units_inv_right {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ} : Commute a ↑u → Commute a ↑u⁻¹

ink

@[simp]

theorem AddCommute.addUnits_neg_right_iff {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M} : AddCommute a ↑(-u) ↔ AddCommute a ↑u

ink

@[simp]

theorem Commute.units_inv_right_iff {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ} : Commute a ↑u⁻¹ ↔ Commute a ↑u

ink

theorem AddCommute.addUnits_neg_left {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M} : AddCommute (↑u) a → AddCommute (↑(-u)) a

ink

theorem Commute.units_inv_left {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ} : Commute (↑u) a → Commute (↑u⁻¹) a

ink

@[simp]

theorem AddCommute.addUnits_neg_left_iff {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M} : AddCommute (↑(-u)) a ↔ AddCommute (↑u) a

ink

@[simp]

theorem Commute.units_inv_left_iff {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ} : Commute (↑u⁻¹) a ↔ Commute (↑u) a

ink

theorem AddCommute.addUnits_val {M : Type u_1} [inst : AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} : AddCommute u₁ u₂ → AddCommute ↑u₁ ↑u₂

ink

theorem Commute.units_val {M : Type u_1} [inst : Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} : Commute u₁ u₂ → Commute ↑u₁ ↑u₂

ink

theorem AddCommute.addUnits_of_val {M : Type u_1} [inst : AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} : AddCommute ↑u₁ ↑u₂ → AddCommute u₁ u₂

ink

theorem Commute.units_of_val {M : Type u_1} [inst : Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} : Commute ↑u₁ ↑u₂ → Commute u₁ u₂

ink

@[simp]

theorem AddCommute.addUnits_val_iff {M : Type u_1} [inst : AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} : AddCommute ↑u₁ ↑u₂ ↔ AddCommute u₁ u₂

ink

@[simp]

theorem Commute.units_val_iff {M : Type u_1} [inst : Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} : Commute ↑u₁ ↑u₂ ↔ Commute u₁ u₂

ink

def AddUnits.leftOfAdd.proof_2 {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = ↑u) (hc : AddCommute a b) : b + ↑(-u) + a = 0

Equations

• (_ : b + ↑(-u) + a = 0) = (_ : b + ↑(-u) + a = 0)

ink

def AddUnits.leftOfAdd.proof_1 {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = ↑u) : a + (b + ↑(-u)) = 0

Equations

• (_ : a + (b + ↑(-u)) = 0) = (_ : a + (b + ↑(-u)) = 0)

ink

def AddUnits.leftOfAdd {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = ↑u) (hc : AddCommute a b) : AddUnits M

If the sum of two commuting elements is an additive unit, then the left summand is an additive unit.

Equations

• AddUnits.leftOfAdd u a b hu hc = { val := a, neg := b + ↑(-u), val_neg := (_ : a + (b + ↑(-u)) = 0), neg_val := (_ : b + ↑(-u) + a = 0) }

ink

def Units.leftOfMul {M : Type u_1} [inst : Monoid M] (u : Mˣ) (a : M) (b : M) (hu : a * b = ↑u) (hc : Commute a b) : Mˣ

If the product of two commuting elements is a unit, then the left multiplier is a unit.

Equations

• Units.leftOfMul u a b hu hc = { val := a, inv := b * ↑u⁻¹, val_inv := (_ : a * (b * ↑u⁻¹) = 1), inv_val := (_ : b * ↑u⁻¹ * a = 1) }

ink

def AddUnits.rightOfAdd.proof_1 {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = ↑u) (hc : AddCommute a b) : b + a = ↑u

Equations

• (_ : b + a = ↑u) = (_ : b + a = ↑u)

ink

def AddUnits.rightOfAdd.proof_2 {M : Type u_1} [inst : AddMonoid M] (a : M) (b : M) (hc : AddCommute a b) : AddCommute b a

Equations

• (_ : AddCommute b a) = (_ : AddCommute b a)

ink

def AddUnits.rightOfAdd {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = ↑u) (hc : AddCommute a b) : AddUnits M

If the sum of two commuting elements is an additive unit, then the right summand is an additive unit.

Equations

• AddUnits.rightOfAdd u a b hu hc = AddUnits.leftOfAdd u b a (_ : b + a = ↑u) (_ : AddCommute b a)

ink

def Units.rightOfMul {M : Type u_1} [inst : Monoid M] (u : Mˣ) (a : M) (b : M) (hu : a * b = ↑u) (hc : Commute a b) : Mˣ

If the product of two commuting elements is a unit, then the right multiplier is a unit.

Equations

• Units.rightOfMul u a b hu hc = Units.leftOfMul u b a (_ : b * a = ↑u) (_ : Commute b a)

ink

theorem AddCommute.isAddUnit_add_iff {M : Type u_1} [inst : AddMonoid M] {a : M} {b : M} (h : AddCommute a b) : IsAddUnit (a + b) ↔ IsAddUnit a ∧ IsAddUnit b

ink

abbrev AddCommute.isAddUnit_add_iff.match_1 {M : Type u_1} [inst : AddMonoid M] {a : M} {b : M} (motive : IsAddUnit (a + b) → Prop) : (x : IsAddUnit (a + b)) → ((u : AddUnits M) → (hu : ↑u = a + b) → motive (_ : ∃ u, ↑u = a + b)) → motive x

Equations

• AddCommute.isAddUnit_add_iff.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

theorem Commute.isUnit_mul_iff {M : Type u_1} [inst : Monoid M] {a : M} {b : M} (h : Commute a b) : IsUnit (a * b) ↔ IsUnit a ∧ IsUnit b

ink

@[simp]

theorem isAddUnit_add_self_iff {M : Type u_1} [inst : AddMonoid M] {a : M} : IsAddUnit (a + a) ↔ IsAddUnit a

ink

@[simp]

theorem isUnit_mul_self_iff {M : Type u_1} [inst : Monoid M] {a : M} : IsUnit (a * a) ↔ IsUnit a

ink

theorem AddCommute.neg_neg {G : Type u_1} [inst : SubtractionMonoid G] {a : G} {b : G} : AddCommute a b → AddCommute (-a) (-b)

ink

theorem Commute.inv_inv {G : Type u_1} [inst : DivisionMonoid G] {a : G} {b : G} : Commute a b → Commute a⁻¹ b⁻¹

ink

@[simp]

theorem AddCommute.neg_neg_iff {G : Type u_1} [inst : SubtractionMonoid G] {a : G} {b : G} : AddCommute (-a) (-b) ↔ AddCommute a b

ink

@[simp]

theorem Commute.inv_inv_iff {G : Type u_1} [inst : DivisionMonoid G] {a : G} {b : G} : Commute a⁻¹ b⁻¹ ↔ Commute a b

ink

theorem AddCommute.add_neg {G : Type u_1} [inst : SubtractionMonoid G] {a : G} {b : G} (hab : AddCommute a b) : -(a + b) = -a + -b

ink

theorem Commute.mul_inv {G : Type u_1} [inst : DivisionMonoid G] {a : G} {b : G} (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹

ink

theorem AddCommute.neg {G : Type u_1} [inst : SubtractionMonoid G] {a : G} {b : G} (hab : AddCommute a b) : -(a + b) = -a + -b

ink

theorem Commute.inv {G : Type u_1} [inst : DivisionMonoid G] {a : G} {b : G} (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹

ink

theorem AddCommute.sub_add_sub_comm {G : Type u_1} [inst : SubtractionMonoid G] {a : G} {b : G} {c : G} {d : G} (hbd : AddCommute b d) (hbc : AddCommute (-b) c) : a - b + (c - d) = a + c - (b + d)

ink

theorem Commute.div_mul_div_comm {G : Type u_1} [inst : DivisionMonoid G] {a : G} {b : G} {c : G} {d : G} (hbd : Commute b d) (hbc : Commute b⁻¹ c) : a / b * (c / d) = a * c / (b * d)

ink

theorem AddCommute.add_sub_add_comm {G : Type u_1} [inst : SubtractionMonoid G] {a : G} {b : G} {c : G} {d : G} (hcd : AddCommute c d) (hbc : AddCommute b (-c)) : a + b - (c + d) = a - c + (b - d)

ink

theorem Commute.mul_div_mul_comm {G : Type u_1} [inst : DivisionMonoid G] {a : G} {b : G} {c : G} {d : G} (hcd : Commute c d) (hbc : Commute b c⁻¹) : a * b / (c * d) = a / c * (b / d)

ink

theorem AddCommute.sub_sub_sub_comm {G : Type u_1} [inst : SubtractionMonoid G] {a : G} {b : G} {c : G} {d : G} (hbc : AddCommute b c) (hbd : AddCommute (-b) d) (hcd : AddCommute (-c) d) : a - b - (c - d) = a - c - (b - d)

ink

theorem Commute.div_div_div_comm {G : Type u_1} [inst : DivisionMonoid G] {a : G} {b : G} {c : G} {d : G} (hbc : Commute b c) (hbd : Commute b⁻¹ d) (hcd : Commute c⁻¹ d) : a / b / (c / d) = a / c / (b / d)

ink

theorem AddCommute.neg_right {G : Type u_1} [inst : AddGroup G] {a : G} {b : G} : AddCommute a b → AddCommute a (-b)

ink

theorem Commute.inv_right {G : Type u_1} [inst : Group G] {a : G} {b : G} : Commute a b → Commute a b⁻¹

ink

@[simp]

theorem AddCommute.neg_right_iff {G : Type u_1} [inst : AddGroup G] {a : G} {b : G} : AddCommute a (-b) ↔ AddCommute a b

ink

@[simp]

theorem Commute.inv_right_iff {G : Type u_1} [inst : Group G] {a : G} {b : G} : Commute a b⁻¹ ↔ Commute a b

ink

theorem AddCommute.neg_left {G : Type u_1} [inst : AddGroup G] {a : G} {b : G} : AddCommute a b → AddCommute (-a) b

ink

theorem Commute.inv_left {G : Type u_1} [inst : Group G] {a : G} {b : G} : Commute a b → Commute a⁻¹ b

ink

@[simp]

theorem AddCommute.neg_left_iff {G : Type u_1} [inst : AddGroup G] {a : G} {b : G} : AddCommute (-a) b ↔ AddCommute a b

ink

@[simp]

theorem Commute.inv_left_iff {G : Type u_1} [inst : Group G] {a : G} {b : G} : Commute a⁻¹ b ↔ Commute a b

ink

theorem AddCommute.neg_add_cancel {G : Type u_1} [inst : AddGroup G] {a : G} {b : G} (h : AddCommute a b) : -a + b + a = b

ink

theorem Commute.inv_mul_cancel {G : Type u_1} [inst : Group G] {a : G} {b : G} (h : Commute a b) : a⁻¹ * b * a = b

ink

theorem AddCommute.neg_add_cancel_assoc {G : Type u_1} [inst : AddGroup G] {a : G} {b : G} (h : AddCommute a b) : -a + (b + a) = b

ink

theorem Commute.inv_mul_cancel_assoc {G : Type u_1} [inst : Group G] {a : G} {b : G} (h : Commute a b) : a⁻¹ * (b * a) = b

ink

theorem AddCommute.add_neg_cancel {G : Type u_1} [inst : AddGroup G] {a : G} {b : G} (h : AddCommute a b) : a + b + -a = b

ink

theorem Commute.mul_inv_cancel {G : Type u_1} [inst : Group G] {a : G} {b : G} (h : Commute a b) : a * b * a⁻¹ = b

ink

theorem AddCommute.add_neg_cancel_assoc {G : Type u_1} [inst : AddGroup G] {a : G} {b : G} (h : AddCommute a b) : a + (b + -a) = b

ink

theorem Commute.mul_inv_cancel_assoc {G : Type u_1} [inst : Group G] {a : G} {b : G} (h : Commute a b) : a * (b * a⁻¹) = b

ink

@[simp]

theorem add_neg_cancel_comm {G : Type u_1} [inst : AddCommGroup G] (a : G) (b : G) : a + b + -a = b

ink

@[simp]

theorem mul_inv_cancel_comm {G : Type u_1} [inst : CommGroup G] (a : G) (b : G) : a * b * a⁻¹ = b

ink

@[simp]

theorem add_neg_cancel_comm_assoc {G : Type u_1} [inst : AddCommGroup G] (a : G) (b : G) : a + (b + -a) = b

ink

@[simp]

theorem mul_inv_cancel_comm_assoc {G : Type u_1} [inst : CommGroup G] (a : G) (b : G) : a * (b * a⁻¹) = b

ink

@[simp]

theorem neg_add_cancel_comm {G : Type u_1} [inst : AddCommGroup G] (a : G) (b : G) : -a + b + a = b

ink

@[simp]

theorem inv_mul_cancel_comm {G : Type u_1} [inst : CommGroup G] (a : G) (b : G) : a⁻¹ * b * a = b

ink

@[simp]

theorem neg_add_cancel_comm_assoc {G : Type u_1} [inst : AddCommGroup G] (a : G) (b : G) : -a + (b + a) = b

ink

@[simp]

theorem inv_mul_cancel_comm_assoc {G : Type u_1} [inst : CommGroup G] (a : G) (b : G) : a⁻¹ * (b * a) = b