/-
Copyright (c) 2019 Neil Strickland. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Neil Strickland, Yury Kudryashov

! This file was ported from Lean 3 source module algebra.group.commute
! leanprover-community/mathlib commit 05101c3df9d9cfe9430edc205860c79b6d660102
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Semiconj

/-!
# 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`.
-/


variable {
G: Type ?u.5
G : 
Type _: Type (?u.5636+1)
Type _}

/-- Two elements commute if `a * b = b * a`. -/
@[to_additive 
AddCommute: {S : Type u_1} → [inst : Add S] → S → S → Prop
AddCommute "Two elements additively commute if `a + b = b + a`"]
def 
Commute: {S : Type u_1} → [inst : Mul S] → S → S → Prop
Commute {
S: Type ?u.8
S : 
Type _: Type (?u.8+1)
Type _} [
Mul: Type ?u.11 → Type ?u.11
Mul 
S: Type ?u.8
S] (
a: S
a 
b: S
b : 
S: Type ?u.8
S) : 
Prop: Type
Prop :=
  
SemiconjBy: {M : Type ?u.23} → [inst : Mul M] → M → M → M → Prop
SemiconjBy 
a: S
a 
b: S
b 
b: S
b
#align commute 
Commute: {S : Type u_1} → [inst : Mul S] → S → S → Prop
Commute
#align add_commute 
AddCommute: {S : Type u_1} → [inst : Add S] → S → S → Prop
AddCommute

namespace Commute

section Mul

variable {
S: Type ?u.194
S : 
Type _: Type (?u.403+1)
Type _} [
Mul: Type ?u.69 → Type ?u.69
Mul 
S: Type ?u.66
S]

/-- Equality behind `Commute a b`; useful for rewriting. -/
@[
to_additive: ∀ {S : Type u_1} [inst : Add S] {a b : S}, AddCommute a b → a + b = b + a
to_additive "Equality behind `add_commute a b`; useful for rewriting."]
protected theorem 
eq: ∀ {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq {
a: S
a 
b: S
b : 
S: Type ?u.75
S} (
h: Commute a b
h : 
Commute: {S : Type ?u.85} → [inst : Mul S] → S → S → Prop
Commute 
a: S
a 
b: S
b) : 
a: S
a * 
b: S
b = 
b: S
b * 
a: S
a :=
  
h: Commute a b
h
#align commute.eq 
Commute.eq: ∀ {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
Commute.eq
#align add_commute.eq 
AddCommute.eq: ∀ {S : Type u_1} [inst : Add S] {a b : S}, AddCommute a b → a + b = b + a
AddCommute.eq

/-- Any element commutes with itself. -/
@[
to_additive: ∀ {S : Type u_1} [inst : Add S] (a : S), AddCommute a a
to_additive (attr := refl, simp) "Any element commutes with itself."]
protected theorem 
refl: ∀ (a : S), Commute a a
refl (
a: S
a : 
S: Type ?u.194
S) : 
Commute: {S : Type ?u.202} → [inst : Mul S] → S → S → Prop
Commute 
a: S
a 
a: S
a :=
  
Eq.refl: ∀ {α : Sort ?u.217} (a : α), a = a
Eq.refl (
a: S
a * 
a: S
a)
#align commute.refl 
Commute.refl: ∀ {S : Type u_1} [inst : Mul S] (a : S), Commute a a
Commute.refl
#align add_commute.refl 
AddCommute.refl: ∀ {S : Type u_1} [inst : Add S] (a : S), AddCommute a a
AddCommute.refl

/-- If `a` commutes with `b`, then `b` commutes with `a`. -/
@[
to_additive: ∀ {S : Type u_1} [inst : Add S] {a b : S}, AddCommute a b → AddCommute b a
to_additive (attr := symm) "If `a` commutes with `b`, then `b` commutes with `a`."]
protected theorem 
symm: ∀ {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b → Commute b a
symm {
a: S
a 
b: S
b : 
S: Type ?u.315
S} (
h: Commute a b
h : 
Commute: {S : Type ?u.325} → [inst : Mul S] → S → S → Prop
Commute 
a: S
a 
b: S
b) : 
Commute: {S : Type ?u.339} → [inst : Mul S] → S → S → Prop
Commute 
b: S
b 
a: S
a :=
  
Eq.symm: ∀ {α : Sort ?u.353} {a b : α}, a = b → b = a
Eq.symm 
h: Commute a b
h
#align commute.symm 
Commute.symm: ∀ {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b → Commute b a
Commute.symm
#align add_commute.symm 
AddCommute.symm: ∀ {S : Type u_1} [inst : Add S] {a b : S}, AddCommute a b → AddCommute b a
AddCommute.symm

@[
to_additive: ∀ {S : Type u_1} [inst : Add S] {a b : S}, AddCommute a b → AddSemiconjBy a b b
to_additive]
protected theorem 
semiconjBy: ∀ {a b : S}, Commute a b → SemiconjBy a b b
semiconjBy {
a: S
a 
b: S
b : 
S: Type ?u.403
S} (
h: Commute a b
h : 
Commute: {S : Type ?u.413} → [inst : Mul S] → S → S → Prop
Commute 
a: S
a 
b: S
b) : 
SemiconjBy: {M : Type ?u.427} → [inst : Mul M] → M → M → M → Prop
SemiconjBy 
a: S
a 
b: S
b 
b: S
b :=
  
h: Commute a b
h
#align commute.semiconj_by 
Commute.semiconjBy: ∀ {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b → SemiconjBy a b b
Commute.semiconjBy
#align add_commute.semiconj_by 
AddCommute.semiconjBy: ∀ {S : Type u_1} [inst : Add S] {a b : S}, AddCommute a b → AddSemiconjBy a b b
AddCommute.semiconjBy

@[
to_additive: ∀ {S : Type u_1} [inst : Add S] {a b : S}, AddCommute a b ↔ AddCommute b a
to_additive]
protected theorem 
symm_iff: ∀ {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b ↔ Commute b a
symm_iff {
a: S
a 
b: S
b : 
S: Type ?u.470
S} : 
Commute: {S : Type ?u.480} → [inst : Mul S] → S → S → Prop
Commute 
a: S
a 
b: S
b ↔ 
Commute: {S : Type ?u.488} → [inst : Mul S] → S → S → Prop
Commute 
b: S
b 
a: S
a :=
  ⟨
Commute.symm: ∀ {S : Type ?u.502} [inst : Mul S] {a b : S}, Commute a b → Commute b a
Commute.symm, 
Commute.symm: ∀ {S : Type ?u.523} [inst : Mul S] {a b : S}, Commute a b → Commute b a
Commute.symm⟩
#align commute.symm_iff 
Commute.symm_iff: ∀ {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b ↔ Commute b a
Commute.symm_iff
#align add_commute.symm_iff 
AddCommute.symm_iff: ∀ {S : Type u_1} [inst : Add S] {a b : S}, AddCommute a b ↔ AddCommute b a
AddCommute.symm_iff

@[
to_additive: ∀ {S : Type u_1} [inst : Add S], IsRefl S AddCommute
to_additive]
instance: ∀ {S : Type u_1} [inst : Mul S], IsRefl S Commute
instance : 
IsRefl: (α : Type ?u.565) → (α → α → Prop) → Prop
IsRefl 
S: Type ?u.559
S 
Commute: {S : Type ?u.566} → [inst : Mul S] → S → S → Prop
Commute :=
  ⟨
Commute.refl: ∀ {S : Type ?u.597} [inst : Mul S] (a : S), Commute a a
Commute.refl⟩

-- This instance is useful for `Finset.noncomm_prod`
@[
to_additive: ∀ {G : Type u_1} {S : Type u_2} [inst : Add S] {f : G → S}, IsRefl G fun a b => AddCommute (f a) (f b)
to_additive]
instance 
on_isRefl: ∀ {f : G → S}, IsRefl G fun a b => Commute (f a) (f b)
on_isRefl {
f: G → S
f : 
G: Type ?u.656
G → 
S: Type ?u.659
S} : 
IsRefl: (α : Type ?u.669) → (α → α → Prop) → Prop
IsRefl 
G: Type ?u.656
G fun 
a: ?m.671
a 
b: ?m.674
b => 
Commute: {S : Type ?u.676} → [inst : Mul S] → S → S → Prop
Commute (
f: G → S
f 
a: ?m.671
a) (
f: G → S
f 
b: ?m.674
b) :=
  ⟨fun 
_: ?m.705
_ => 
Commute.refl: ∀ {S : Type ?u.707} [inst : Mul S] (a : S), Commute a a
Commute.refl 
_: ?m.708
_⟩
#align commute.on_is_refl 
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)
Commute.on_isRefl
#align add_commute.on_is_refl 
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)
AddCommute.on_isRefl

end Mul

section Semigroup

variable {
S: Type ?u.806
S : 
Type _: Type (?u.1763+1)
Type _} [
Semigroup: Type ?u.809 → Type ?u.809
Semigroup 
S: Type ?u.806
S] {
a: S
a 
b: S
b 
c: S
c : 
S: Type ?u.806
S}

/-- If `a` commutes with both `b` and `c`, then it commutes with their product. -/
@[
to_additive: ∀ {S : Type u_1} [inst : AddSemigroup S] {a b c : S}, AddCommute a b → AddCommute a c → AddCommute a (b + c)
to_additive (attr := simp)
"If `a` commutes with both `b` and `c`, then it commutes with their sum."]
theorem 
mul_right: ∀ {S : Type u_1} [inst : Semigroup S] {a b c : S}, Commute a b → Commute a c → Commute a (b * c)
mul_right (
hab: Commute a b
hab : 
Commute: {S : Type ?u.833} → [inst : Mul S] → S → S → Prop
Commute 
a: S
a 
b: S
b) (
hac: Commute a c
hac : 
Commute: {S : Type ?u.948} → [inst : Mul S] → S → S → Prop
Commute 
a: S
a 
c: S
c) : 
Commute: {S : Type ?u.957} → [inst : Mul S] → S → S → Prop
Commute 
a: S
a (
b: S
b * 
c: S
c) :=
  
SemiconjBy.mul_right: ∀ {S : Type ?u.1153} [inst : Semigroup S] {a x y x' y' : S},
  SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x * x') (y * y')
SemiconjBy.mul_right 
hab: Commute a b
hab 
hac: Commute a c
hac
#align commute.mul_right 
Commute.mul_rightₓ: ∀ {S : Type u_1} [inst : Semigroup S] {a b c : S}, Commute a b → Commute a c → Commute a (b * c)
Commute.mul_rightₓ
#align add_commute.add_right 
AddCommute.add_rightₓ: ∀ {S : Type u_1} [inst : AddSemigroup S] {a b c : S}, AddCommute a b → AddCommute a c → AddCommute a (b + c)
AddCommute.add_rightₓ
-- I think `ₓ` is necessary because of the `mul` vs `HMul` distinction

/-- If both `a` and `b` commute with `c`, then their product commutes with `c`. -/
@[
to_additive: ∀ {S : Type u_1} [inst : AddSemigroup S] {a b c : S}, AddCommute a c → AddCommute b c → AddCommute (a + b) c
to_additive (attr := simp)
"If both `a` and `b` commute with `c`, then their product commutes with `c`."]
theorem 
mul_left: ∀ {S : Type u_1} [inst : Semigroup S] {a b c : S}, Commute a c → Commute b c → Commute (a * b) c
mul_left (
hac: Commute a c
hac : 
Commute: {S : Type ?u.1304} → [inst : Mul S] → S → S → Prop
Commute 
a: S
a 
c: S
c) (
hbc: Commute b c
hbc : 
Commute: {S : Type ?u.1419} → [inst : Mul S] → S → S → Prop
Commute 
b: S
b 
c: S
c) : 
Commute: {S : Type ?u.1428} → [inst : Mul S] → S → S → Prop
Commute (
a: S
a * 
b: S
b) 
c: S
c :=
  
SemiconjBy.mul_left: ∀ {S : Type ?u.1624} [inst : Semigroup S] {a b x y z : S}, SemiconjBy a y z → SemiconjBy b x y → SemiconjBy (a * b) x z
SemiconjBy.mul_left 
hac: Commute a c
hac 
hbc: Commute b c
hbc
#align commute.mul_left 
Commute.mul_leftₓ: ∀ {S : Type u_1} [inst : Semigroup S] {a b c : S}, Commute a c → Commute b c → Commute (a * b) c
Commute.mul_leftₓ
#align add_commute.add_left 
AddCommute.add_leftₓ: ∀ {S : Type u_1} [inst : AddSemigroup S] {a b c : S}, AddCommute a c → AddCommute b c → AddCommute (a + b) c
AddCommute.add_leftₓ
-- I think `ₓ` is necessary because of the `mul` vs `HMul` distinction

@[
to_additive: ∀ {S : Type u_1} [inst : AddSemigroup S] {b c : S}, AddCommute b c → ∀ (a : S), a + b + c = a + c + b
to_additive]
protected theorem 
right_comm: Commute b c → ∀ (a : S), a * b * c = a * c * b
right_comm (
h: Commute b c
h : 
Commute: {S : Type ?u.1775} → [inst : Mul S] → S → S → Prop
Commute 
b: S
b 
c: S
c) (
a: S
a : 
S: Type ?u.1763
S) : 
a: S
a * 
b: S
b * 
c: S
c = 
a: S
a * 
c: S
c * 
b: S
b :=
  by
Goals accomplished! 🐙 
G: Type ?u.1760

S: Type u_1

inst✝: Semigroup S

a✝, b, c: S

h: Commute b c

a: S

a * b * c = a * c * bsimp only [
mul_assoc: ∀ {G : Type ?u.2385} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc, 
h: Commute b c
h.
eq: ∀ {S : Type ?u.2404} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq]
Goals accomplished! 🐙
#align commute.right_comm 
Commute.right_commₓ: ∀ {S : Type u_1} [inst : Semigroup S] {b c : S}, Commute b c → ∀ (a : S), a * b * c = a * c * b
Commute.right_commₓ
#align add_commute.right_comm 
AddCommute.right_commₓ: ∀ {S : Type u_1} [inst : AddSemigroup S] {b c : S}, AddCommute b c → ∀ (a : S), a + b + c = a + c + b
AddCommute.right_commₓ
-- I think `ₓ` is necessary because of the `mul` vs `HMul` distinction

@[
to_additive: ∀ {S : Type u_1} [inst : AddSemigroup S] {a b : S}, AddCommute a b → ∀ (c : S), a + (b + c) = b + (a + c)
to_additive]
protected theorem 
left_comm: Commute a b → ∀ (c : S), a * (b * c) = b * (a * c)
left_comm (
h: Commute a b
h : 
Commute: {S : Type ?u.2646} → [inst : Mul S] → S → S → Prop
Commute 
a: S
a 
b: S
b) (
c: ?m.2761
c) : 
a: S
a * (
b: S
b * 
c: ?m.2761
c) = 
b: S
b * (
a: S
a * 
c: ?m.2761
c) :=
  by
Goals accomplished! 🐙 
G: Type ?u.2631

S: Type u_1

inst✝: Semigroup S

a, b, c✝: S

h: Commute a b

c: S

a * (b * c) = b * (a * c)simp only [← 
mul_assoc: ∀ {G : Type ?u.3257} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc, 
h: Commute a b
h.
eq: ∀ {S : Type ?u.3281} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq]
Goals accomplished! 🐙
#align commute.left_comm 
Commute.left_commₓ: ∀ {S : Type u_1} [inst : Semigroup S] {a b : S}, Commute a b → ∀ (c : S), a * (b * c) = b * (a * c)
Commute.left_commₓ
#align add_commute.left_comm 
AddCommute.left_commₓ: ∀ {S : Type u_1} [inst : AddSemigroup S] {a b : S}, AddCommute a b → ∀ (c : S), a + (b + c) = b + (a + c)
AddCommute.left_commₓ
-- I think `ₓ` is necessary because of the `mul` vs `HMul` distinction

@[
to_additive: ∀ {S : Type u_1} [inst : AddSemigroup S] {b c : S}, AddCommute b c → ∀ (a d : S), a + b + (c + d) = a + c + (b + d)
to_additive]
protected theorem 
mul_mul_mul_comm: Commute b c → ∀ (a d : S), a * b * (c * d) = a * c * (b * d)
mul_mul_mul_comm (
hbc: Commute b c
hbc : 
Commute: {S : Type ?u.3544} → [inst : Mul S] → S → S → Prop
Commute 
b: S
b 
c: S
c) (
a: S
a 
d: S
d : 
S: Type ?u.3532
S) :
    
a: S
a * 
b: S
b * (
c: S
c * 
d: S
d) = 
a: S
a * 
c: S
c * (
b: S
b * 
d: S
d) := by
Goals accomplished! 🐙 
G: Type ?u.3529

S: Type u_1

inst✝: Semigroup S

a✝, b, c: S

hbc: Commute b c

a, d: S

a * b * (c * d) = a * c * (b * d)simp only [
hbc: Commute b c
hbc.
left_comm: ∀ {S : Type ?u.4352} [inst : Semigroup S] {a b : S}, Commute a b → ∀ (c : S), a * (b * c) = b * (a * c)
left_comm, 
mul_assoc: ∀ {G : Type ?u.4382} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc]
Goals accomplished! 🐙
#align commute.mul_mul_mul_comm 
Commute.mul_mul_mul_comm: ∀ {S : Type u_1} [inst : Semigroup S] {b c : S}, Commute b c → ∀ (a d : S), a * b * (c * d) = a * c * (b * d)
Commute.mul_mul_mul_comm
#align add_commute.add_add_add_comm 
AddCommute.add_add_add_comm: ∀ {S : Type u_1} [inst : AddSemigroup S] {b c : S}, AddCommute b c → ∀ (a d : S), a + b + (c + d) = a + c + (b + d)
AddCommute.add_add_add_comm

end Semigroup

@[
to_additive: ∀ {S : Type u_1} [inst : AddCommSemigroup S] (a b : S), AddCommute a b
to_additive]
protected theorem 
all: ∀ {S : Type u_1} [inst : CommSemigroup S] (a b : S), Commute a b
all {
S: Type ?u.4513
S : 
Type _: Type (?u.4513+1)
Type _} [
CommSemigroup: Type ?u.4516 → Type ?u.4516
CommSemigroup 
S: Type ?u.4513
S] (
a: S
a 
b: S
b : 
S: Type ?u.4513
S) : 
Commute: {S : Type ?u.4523} → [inst : Mul S] → S → S → Prop
Commute 
a: S
a 
b: S
b :=
  
mul_comm: ∀ {G : Type ?u.4666} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm 
a: S
a 
b: S
b
#align commute.all 
Commute.allₓ: ∀ {S : Type u_1} [inst : CommSemigroup S] (a b : S), Commute a b
Commute.allₓ
#align add_commute.all 
AddCommute.allₓ: ∀ {S : Type u_1} [inst : AddCommSemigroup S] (a b : S), AddCommute a b
AddCommute.allₓ
-- not sure why this needs an `ₓ`, maybe instance names not aligned?

section MulOneClass

variable {
M: Type ?u.4705
M : 
Type _: Type (?u.4705+1)
Type _} [
MulOneClass: Type ?u.4708 → Type ?u.4708
MulOneClass 
M: Type ?u.4705
M]

@[
to_additive: ∀ {M : Type u_1} [inst : AddZeroClass M] (a : M), AddCommute a 0
to_additive (attr := simp)]
theorem 
one_right: ∀ (a : M), Commute a 1
one_right (
a: M
a : 
M: Type ?u.4705
M) : 
Commute: {S : Type ?u.4713} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a 
1: ?m.4721
1 :=
  
SemiconjBy.one_right: ∀ {M : Type ?u.4854} [inst : MulOneClass M] (a : M), SemiconjBy a 1 1
SemiconjBy.one_right 
a: M
a
#align commute.one_right 
Commute.one_rightₓ: ∀ {M : Type u_1} [inst : MulOneClass M] (a : M), Commute a 1
Commute.one_rightₓ
#align add_commute.zero_right 
AddCommute.zero_rightₓ: ∀ {M : Type u_1} [inst : AddZeroClass M] (a : M), AddCommute a 0
AddCommute.zero_rightₓ
-- I think `ₓ` is necessary because `One.toOfNat1` appears in the Lean 4 version

@[
to_additive: ∀ {M : Type u_1} [inst : AddZeroClass M] (a : M), AddCommute 0 a
to_additive (attr := simp)]
theorem 
one_left: ∀ {M : Type u_1} [inst : MulOneClass M] (a : M), Commute 1 a
one_left (
a: M
a : 
M: Type ?u.4914
M) : 
Commute: {S : Type ?u.4922} → [inst : Mul S] → S → S → Prop
Commute 
1: ?m.4930
1 
a: M
a :=
  
SemiconjBy.one_left: ∀ {M : Type ?u.5069} [inst : MulOneClass M] (x : M), SemiconjBy 1 x x
SemiconjBy.one_left 
a: M
a
#align commute.one_left 
Commute.one_leftₓ: ∀ {M : Type u_1} [inst : MulOneClass M] (a : M), Commute 1 a
Commute.one_leftₓ
#align add_commute.zero_left 
AddCommute.zero_leftₓ: ∀ {M : Type u_1} [inst : AddZeroClass M] (a : M), AddCommute 0 a
AddCommute.zero_leftₓ
-- I think `ₓ` is necessary because `One.toOfNat1` appears in the Lean 4 version

end MulOneClass

section Monoid

variable {
M: Type ?u.5129
M : 
Type _: Type (?u.8434+1)
Type _} [
Monoid: Type ?u.7760 → Type ?u.7760
Monoid 
M: Type ?u.9814
M] {
a: M
a 
b: M
b : 
M: Type ?u.6153
M} {
u: Mˣ
u 
u₁: Mˣ
u₁ 
u₂: Mˣ
u₂ : 
M: Type ?u.5129
Mˣ}

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (n : ℕ), AddCommute a (n • b)
to_additive (attr := simp)]
theorem 
pow_right: ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute a (b ^ n)
pow_right (
h: Commute a b
h : 
Commute: {S : Type ?u.5190} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a 
b: M
b) (
n: ℕ
n : 
ℕ: Type
ℕ) : 
Commute: {S : Type ?u.5220} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a (
b: M
b ^ 
n: ℕ
n) :=
  
SemiconjBy.pow_right: ∀ {M : Type ?u.5523} [inst : Monoid M] {a x y : M}, SemiconjBy a x y → ∀ (n : ℕ), SemiconjBy a (x ^ n) (y ^ n)
SemiconjBy.pow_right 
h: Commute a b
h 
n: ℕ
n
#align commute.pow_right 
Commute.pow_rightₓ: ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute a (b ^ n)
Commute.pow_rightₓ
#align add_commute.nsmul_right 
AddCommute.nsmul_rightₓ: ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (n : ℕ), AddCommute a (n • b)
AddCommute.nsmul_rightₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (n : ℕ), AddCommute (n • a) b
to_additive (attr := simp)]
theorem 
pow_left: Commute a b → ∀ (n : ℕ), Commute (a ^ n) b
pow_left (
h: Commute a b
h : 
Commute: {S : Type ?u.5668} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a 
b: M
b) (
n: ℕ
n : 
ℕ: Type
ℕ) : 
Commute: {S : Type ?u.5698} → [inst : Mul S] → S → S → Prop
Commute (
a: M
a ^ 
n: ℕ
n) 
b: M
b :=
  (
h: Commute a b
h.
symm: ∀ {S : Type ?u.6001} [inst : Mul S] {a b : S}, Commute a b → Commute b a
symm.
pow_right: ∀ {M : Type ?u.6029} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute a (b ^ n)
pow_right 
n: ℕ
n).
symm: ∀ {S : Type ?u.6051} [inst : Mul S] {a b : S}, Commute a b → Commute b a
symm
#align commute.pow_left 
Commute.pow_leftₓ: ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute (a ^ n) b
Commute.pow_leftₓ
#align add_commute.nsmul_left 
AddCommute.nsmul_leftₓ: ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (n : ℕ), AddCommute (n • a) b
AddCommute.nsmul_leftₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`

-- todo: should nat power be called `nsmul` here?
@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (m n : ℕ), AddCommute (m • a) (n • b)
to_additive (attr := simp)]
theorem 
pow_pow: Commute a b → ∀ (m n : ℕ), Commute (a ^ m) (b ^ n)
pow_pow (
h: Commute a b
h : 
Commute: {S : Type ?u.6182} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a 
b: M
b) (
m: ℕ
m 
n: ℕ
n : 
ℕ: Type
ℕ) : 
Commute: {S : Type ?u.6214} → [inst : Mul S] → S → S → Prop
Commute (
a: M
a ^ 
m: ℕ
m) (
b: M
b ^ 
n: ℕ
n) :=
  (
h: Commute a b
h.
pow_left: ∀ {M : Type ?u.6759} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute (a ^ n) b
pow_left 
m: ℕ
m).
pow_right: ∀ {M : Type ?u.6787} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute a (b ^ n)
pow_right 
n: ℕ
n
#align commute.pow_pow 
Commute.pow_powₓ: ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b → ∀ (m n : ℕ), Commute (a ^ m) (b ^ n)
Commute.pow_powₓ
#align add_commute.nsmul_nsmul 
AddCommute.nsmul_nsmulₓ: ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (m n : ℕ), AddCommute (m • a) (n • b)
AddCommute.nsmul_nsmulₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`

-- porting note: `simpNF` told me to remove the `simp` attribute
@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ), AddCommute a (n • a)
to_additive]
theorem 
self_pow: ∀ {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ), Commute a (a ^ n)
self_pow (
a: M
a : 
M: Type ?u.6903
M) (
n: ℕ
n : 
ℕ: Type
ℕ) : 
Commute: {S : Type ?u.6936} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a (
a: M
a ^ 
n: ℕ
n) :=
  (
Commute.refl: ∀ {S : Type ?u.7258} [inst : Mul S] (a : S), Commute a a
Commute.refl 
a: M
a).
pow_right: ∀ {M : Type ?u.7280} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute a (b ^ n)
pow_right 
n: ℕ
n
#align commute.self_pow 
Commute.self_powₓ: ∀ {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ), Commute a (a ^ n)
Commute.self_powₓ
#align add_commute.self_nsmul 
AddCommute.self_nsmulₓ: ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ), AddCommute a (n • a)
AddCommute.self_nsmulₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`

-- porting note: `simpNF` told me to remove the `simp` attribute
@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ), AddCommute (n • a) a
to_additive]
theorem 
pow_self: ∀ (a : M) (n : ℕ), Commute (a ^ n) a
pow_self (
a: M
a : 
M: Type ?u.7330
M) (
n: ℕ
n : 
ℕ: Type
ℕ) : 
Commute: {S : Type ?u.7363} → [inst : Mul S] → S → S → Prop
Commute (
a: M
a ^ 
n: ℕ
n) 
a: M
a :=
  (
Commute.refl: ∀ {S : Type ?u.7685} [inst : Mul S] (a : S), Commute a a
Commute.refl 
a: M
a).
pow_left: ∀ {M : Type ?u.7707} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute (a ^ n) b
pow_left 
n: ℕ
n
#align add_commute.nsmul_self 
AddCommute.nsmul_selfₓ: ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ), AddCommute (n • a) a
AddCommute.nsmul_selfₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`
#align commute.pow_self 
Commute.pow_self: ∀ {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ), Commute (a ^ n) a
Commute.pow_self

-- porting note: `simpNF` told me to remove the `simp` attribute
@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (m n : ℕ), AddCommute (m • a) (n • a)
to_additive]
theorem 
pow_pow_self: ∀ {M : Type u_1} [inst : Monoid M] (a : M) (m n : ℕ), Commute (a ^ m) (a ^ n)
pow_pow_self (
a: M
a : 
M: Type ?u.7757
M) (
m: ℕ
m 
n: ℕ
n : 
ℕ: Type
ℕ) : 
Commute: {S : Type ?u.7792} → [inst : Mul S] → S → S → Prop
Commute (
a: M
a ^ 
m: ℕ
m) (
a: M
a ^ 
n: ℕ
n) :=
  (
Commute.refl: ∀ {S : Type ?u.8356} [inst : Mul S] (a : S), Commute a a
Commute.refl 
a: M
a).
pow_pow: ∀ {M : Type ?u.8378} [inst : Monoid M] {a b : M}, Commute a b → ∀ (m n : ℕ), Commute (a ^ m) (b ^ n)
pow_pow 
m: ℕ
m 
n: ℕ
n
#align commute.pow_pow_self 
Commute.pow_pow_selfₓ: ∀ {M : Type u_1} [inst : Monoid M] (a : M) (m n : ℕ), Commute (a ^ m) (a ^ n)
Commute.pow_pow_selfₓ
#align add_commute.nsmul_nsmul_self 
AddCommute.nsmul_nsmul_selfₓ: ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (m n : ℕ), AddCommute (m • a) (n • a)
AddCommute.nsmul_nsmul_selfₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`

@[to_additive 
succ_nsmul': ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ), (n + 1) • a = n • a + a
succ_nsmul']
theorem 
_root_.pow_succ': ∀ {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a ^ n * a
_root_.pow_succ' (
a: M
a : 
M: Type ?u.8434
M) (
n: ℕ
n : 
ℕ: Type
ℕ) : 
a: M
a ^ (
n: ℕ
n + 
1: ?m.8475
1) = 
a: M
a ^ 
n: ℕ
n * 
a: M
a :=
  (
pow_succ: ∀ {M : Type ?u.8963} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
pow_succ 
a: M
a 
n: ℕ
n).
trans: ∀ {α : Sort ?u.8973} {a b c : α}, a = b → b = c → a = c
trans (
self_pow: ∀ {M : Type ?u.8987} [inst : Monoid M] (a : M) (n : ℕ), Commute a (a ^ n)
self_pow 
_: ?m.8988
_ 
_: ℕ
_)
#align pow_succ' 
pow_succ': ∀ {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a ^ n * a
pow_succ'
#align succ_nsmul' 
succ_nsmul': ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ), (n + 1) • a = n • a + a
succ_nsmul'

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute a ↑u → AddCommute a ↑(-u)
to_additive]
theorem 
units_inv_right: Commute a ↑u → Commute a ↑u⁻¹
units_inv_right : 
Commute: {S : Type ?u.9071} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a 
u: Mˣ
u → 
Commute: {S : Type ?u.9226} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a ↑
u: Mˣ
u⁻¹ :=
  
SemiconjBy.units_inv_right: ∀ {M : Type ?u.9348} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x ↑y → SemiconjBy a ↑x⁻¹ ↑y⁻¹
SemiconjBy.units_inv_right
#align commute.units_inv_right 
Commute.units_inv_right: ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute a ↑u → Commute a ↑u⁻¹
Commute.units_inv_right
#align add_commute.add_units_neg_right 
AddCommute.addUnits_neg_right: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute a ↑u → AddCommute a ↑(-u)
AddCommute.addUnits_neg_right

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute a ↑(-u) ↔ AddCommute a ↑u
to_additive (attr := simp)]
theorem 
units_inv_right_iff: Commute a ↑u⁻¹ ↔ Commute a ↑u
units_inv_right_iff : 
Commute: {S : Type ?u.9437} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a ↑
u: Mˣ
u⁻¹ ↔ 
Commute: {S : Type ?u.9599} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a 
u: Mˣ
u :=
  
SemiconjBy.units_inv_right_iff: ∀ {M : Type ?u.9704} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x⁻¹ ↑y⁻¹ ↔ SemiconjBy a ↑x ↑y
SemiconjBy.units_inv_right_iff
#align commute.units_inv_right_iff 
Commute.units_inv_right_iff: ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute a ↑u⁻¹ ↔ Commute a ↑u
Commute.units_inv_right_iff
#align add_commute.add_units_neg_right_iff 
AddCommute.addUnits_neg_right_iff: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute a ↑(-u) ↔ AddCommute a ↑u
AddCommute.addUnits_neg_right_iff

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute (↑u) a → AddCommute (↑(-u)) a
to_additive]
theorem 
units_inv_left: ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute (↑u) a → Commute (↑u⁻¹) a
units_inv_left : 
Commute: {S : Type ?u.9844} → [inst : Mul S] → S → S → Prop
Commute (↑
u: Mˣ
u) 
a: M
a → 
Commute: {S : Type ?u.9872} → [inst : Mul S] → S → S → Prop
Commute (↑
u: Mˣ
u⁻¹) 
a: M
a :=
  
SemiconjBy.units_inv_symm_left: ∀ {M : Type ?u.10123} [inst : Monoid M] {a : Mˣ} {x y : M}, SemiconjBy (↑a) x y → SemiconjBy (↑a⁻¹) y x
SemiconjBy.units_inv_symm_left
#align commute.units_inv_left 
Commute.units_inv_left: ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute (↑u) a → Commute (↑u⁻¹) a
Commute.units_inv_left
#align add_commute.add_units_neg_left 
AddCommute.addUnits_neg_left: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute (↑u) a → AddCommute (↑(-u)) a
AddCommute.addUnits_neg_left

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute (↑(-u)) a ↔ AddCommute (↑u) a
to_additive (attr := simp)]
theorem 
units_inv_left_iff: Commute (↑u⁻¹) a ↔ Commute (↑u) a
units_inv_left_iff : 
Commute: {S : Type ?u.10212} → [inst : Mul S] → S → S → Prop
Commute (↑
u: Mˣ
u⁻¹) 
a: M
a ↔ 
Commute: {S : Type ?u.10235} → [inst : Mul S] → S → S → Prop
Commute (↑
u: Mˣ
u) 
a: M
a :=
  
SemiconjBy.units_inv_symm_left_iff: ∀ {M : Type ?u.10481} [inst : Monoid M] {a : Mˣ} {x y : M}, SemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y
SemiconjBy.units_inv_symm_left_iff
#align commute.units_inv_left_iff 
Commute.units_inv_left_iff: ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute (↑u⁻¹) a ↔ Commute (↑u) a
Commute.units_inv_left_iff
#align add_commute.add_units_neg_left_iff 
AddCommute.addUnits_neg_left_iff: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute (↑(-u)) a ↔ AddCommute (↑u) a
AddCommute.addUnits_neg_left_iff

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {u₁ u₂ : AddUnits M}, AddCommute u₁ u₂ → AddCommute ↑u₁ ↑u₂
to_additive]
theorem 
units_val: Commute u₁ u₂ → Commute ↑u₁ ↑u₂
units_val : 
Commute: {S : Type ?u.10621} → [inst : Mul S] → S → S → Prop
Commute 
u₁: Mˣ
u₁ 
u₂: Mˣ
u₂ → 
Commute: {S : Type ?u.10648} → [inst : Mul S] → S → S → Prop
Commute (
u₁: Mˣ
u₁ : 
M: Type ?u.10591
M) 
u₂: Mˣ
u₂ :=
  
SemiconjBy.units_val: ∀ {M : Type ?u.10896} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy a x y → SemiconjBy ↑a ↑x ↑y
SemiconjBy.units_val
#align commute.units_coe 
Commute.units_val: ∀ {M : Type u_1} [inst : Monoid M] {u₁ u₂ : Mˣ}, Commute u₁ u₂ → Commute ↑u₁ ↑u₂
Commute.units_val
#align add_commute.add_units_coe 
AddCommute.addUnits_val: ∀ {M : Type u_1} [inst : AddMonoid M] {u₁ u₂ : AddUnits M}, AddCommute u₁ u₂ → AddCommute ↑u₁ ↑u₂
AddCommute.addUnits_val

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {u₁ u₂ : AddUnits M}, AddCommute ↑u₁ ↑u₂ → AddCommute u₁ u₂
to_additive]
theorem 
units_of_val: ∀ {M : Type u_1} [inst : Monoid M] {u₁ u₂ : Mˣ}, Commute ↑u₁ ↑u₂ → Commute u₁ u₂
units_of_val : 
Commute: {S : Type ?u.10983} → [inst : Mul S] → S → S → Prop
Commute (
u₁: Mˣ
u₁ : 
M: Type ?u.10953
M) 
u₂: Mˣ
u₂ → 
Commute: {S : Type ?u.11240} → [inst : Mul S] → S → S → Prop
Commute 
u₁: Mˣ
u₁ 
u₂: Mˣ
u₂ :=
  
SemiconjBy.units_of_val: ∀ {M : Type ?u.11258} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy ↑a ↑x ↑y → SemiconjBy a x y
SemiconjBy.units_of_val
#align commute.units_of_coe 
Commute.units_of_val: ∀ {M : Type u_1} [inst : Monoid M] {u₁ u₂ : Mˣ}, Commute ↑u₁ ↑u₂ → Commute u₁ u₂
Commute.units_of_val
#align add_commute.add_units_of_coe 
AddCommute.addUnits_of_val: ∀ {M : Type u_1} [inst : AddMonoid M] {u₁ u₂ : AddUnits M}, AddCommute ↑u₁ ↑u₂ → AddCommute u₁ u₂
AddCommute.addUnits_of_val

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {u₁ u₂ : AddUnits M}, AddCommute ↑u₁ ↑u₂ ↔ AddCommute u₁ u₂
to_additive (attr := simp)]
theorem 
units_val_iff: ∀ {M : Type u_1} [inst : Monoid M] {u₁ u₂ : Mˣ}, Commute ↑u₁ ↑u₂ ↔ Commute u₁ u₂
units_val_iff : 
Commute: {S : Type ?u.11347} → [inst : Mul S] → S → S → Prop
Commute (
u₁: Mˣ
u₁ : 
M: Type ?u.11318
M) 
u₂: Mˣ
u₂ ↔ 
Commute: {S : Type ?u.11599} → [inst : Mul S] → S → S → Prop
Commute 
u₁: Mˣ
u₁ 
u₂: Mˣ
u₂ :=
  
SemiconjBy.units_val_iff: ∀ {M : Type ?u.11612} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy ↑a ↑x ↑y ↔ SemiconjBy a x y
SemiconjBy.units_val_iff
#align commute.units_coe_iff 
Commute.units_val_iff: ∀ {M : Type u_1} [inst : Monoid M] {u₁ u₂ : Mˣ}, Commute ↑u₁ ↑u₂ ↔ Commute u₁ u₂
Commute.units_val_iff
#align add_commute.add_units_coe_iff 
AddCommute.addUnits_val_iff: ∀ {M : Type u_1} [inst : AddMonoid M] {u₁ u₂ : AddUnits M}, AddCommute ↑u₁ ↑u₂ ↔ AddCommute u₁ u₂
AddCommute.addUnits_val_iff

/-- If the product of two commuting elements is a unit, then the left multiplier is a unit. -/
@[
to_additive: {M : Type u_1} → [inst : AddMonoid M] → (u : AddUnits M) → (a b : M) → a + b = ↑u → AddCommute a b → AddUnits M
to_additive "If the sum of two commuting elements is an additive unit, then the left summand is
an additive unit."]
def 
_root_.Units.leftOfMul: (u : Mˣ) → (a b : M) → a * b = ↑u → Commute a b → Mˣ
_root_.Units.leftOfMul (
u: Mˣ
u : 
M: Type ?u.11709
Mˣ) (
a: M
a 
b: M
b : 
M: Type ?u.11709
M) (
hu: a * b = ↑u
hu : 
a: M
a * 
b: M
b = 
u: Mˣ
u) (
hc: Commute a b
hc : 
Commute: {S : Type ?u.12046} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a 
b: M
b) : 
M: Type ?u.11709
Mˣ where
  val := 
a: M
a
  inv := 
b: M
b * ↑
u: Mˣ
u⁻¹
  val_inv := by
Goals accomplished! 🐙 
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

a * (b * ↑u⁻¹) = 1rw [
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

a * (b * ↑u⁻¹) = 1← 
mul_assoc: ∀ {G : Type ?u.12230} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc,
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

a * b * ↑u⁻¹ = 1 
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

a * (b * ↑u⁻¹) = 1
hu: a * b = ↑u
hu,
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

↑u * ↑u⁻¹ = 1 
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

a * (b * ↑u⁻¹) = 1
u: Mˣ
u.
mul_inv: ∀ {α : Type ?u.12289} [inst : Monoid α] (a : αˣ), ↑a * ↑a⁻¹ = 1
mul_inv
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

1 = 1]
Goals accomplished! 🐙
  inv_val := by
Goals accomplished! 🐙
    
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

b * ↑u⁻¹ * a = 1have : 
Commute: {S : Type ?u.12303} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a 
u: Mˣ
u := 
hu: a * b = ↑u
hu ▸ (
Commute.refl: ∀ {S : Type ?u.12411} [inst : Mul S] (a : S), Commute a a
Commute.refl 
_: ?m.12412
_).
mul_right: ∀ {S : Type ?u.12419} [inst : Semigroup S] {a b c : S}, Commute a b → Commute a c → Commute a (b * c)
mul_right 
hc: Commute a b
hc
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

this: Commute a ↑u

b * ↑u⁻¹ * a = 1
    
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

b * ↑u⁻¹ * a = 1rw [
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

this: Commute a ↑u

b * ↑u⁻¹ * a = 1← 
this: Commute a ↑u
this.
units_inv_right: ∀ {M : Type ?u.12476} [inst : Monoid M] {a : M} {u : Mˣ}, Commute a ↑u → Commute a ↑u⁻¹
units_inv_right.
right_comm: ∀ {S : Type ?u.12486} [inst : Semigroup S] {b c : S}, Commute b c → ∀ (a : S), a * b * c = a * c * b
right_comm,
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

this: Commute a ↑u

b * a * ↑u⁻¹ = 1 
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

this: Commute a ↑u

b * ↑u⁻¹ * a = 1← 
hc: Commute a b
hc.
eq: ∀ {S : Type ?u.12502} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq,
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

this: Commute a ↑u

a * b * ↑u⁻¹ = 1 
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

this: Commute a ↑u

b * ↑u⁻¹ * a = 1
hu: a * b = ↑u
hu,
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

this: Commute a ↑u

↑u * ↑u⁻¹ = 1 
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

this: Commute a ↑u

b * ↑u⁻¹ * a = 1
u: Mˣ
u.
mul_inv: ∀ {α : Type ?u.12518} [inst : Monoid α] (a : αˣ), ↑a * ↑a⁻¹ = 1
mul_inv
G: Type ?u.11706

M: Type ?u.11709

inst✝: Monoid M

a✝, b✝: M

u✝, u₁, u₂, u: Mˣ

a, b: M

hu: a * b = ↑u

hc: Commute a b

this: Commute a ↑u

1 = 1]
Goals accomplished! 🐙
#align units.left_of_mul 
Units.leftOfMul: {M : Type u_1} → [inst : Monoid M] → (u : Mˣ) → (a b : M) → a * b = ↑u → Commute a b → Mˣ
Units.leftOfMul
#align add_units.left_of_add 
AddUnits.leftOfAdd: {M : Type u_1} → [inst : AddMonoid M] → (u : AddUnits M) → (a b : M) → a + b = ↑u → AddCommute a b → AddUnits M
AddUnits.leftOfAdd

/-- If the product of two commuting elements is a unit, then the right multiplier is a unit. -/
@[
to_additive: {M : Type u_1} → [inst : AddMonoid M] → (u : AddUnits M) → (a b : M) → a + b = ↑u → AddCommute a b → AddUnits M
to_additive "If the sum of two commuting elements is an additive unit, then the right summand
is an additive unit."]
def 
_root_.Units.rightOfMul: {M : Type u_1} → [inst : Monoid M] → (u : Mˣ) → (a b : M) → a * b = ↑u → Commute a b → Mˣ
_root_.Units.rightOfMul (
u: Mˣ
u : 
M: Type ?u.12890
Mˣ) (
a: M
a 
b: M
b : 
M: Type ?u.12890
M) (
hu: a * b = ↑u
hu : 
a: M
a * 
b: M
b = 
u: Mˣ
u) (
hc: Commute a b
hc : 
Commute: {S : Type ?u.13227} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a 
b: M
b) : 
M: Type ?u.12890
Mˣ :=
  
u: Mˣ
u.
leftOfMul: {M : Type ?u.13256} → [inst : Monoid M] → (u : Mˣ) → (a b : M) → a * b = ↑u → Commute a b → Mˣ
leftOfMul 
b: M
b 
a: M
a (
hc: Commute a b
hc.
eq: ∀ {S : Type ?u.13266} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq ▸ 
hu: a * b = ↑u
hu) 
hc: Commute a b
hc.
symm: ∀ {S : Type ?u.13289} [inst : Mul S] {a b : S}, Commute a b → Commute b a
symm
#align units.right_of_mul 
Units.rightOfMul: {M : Type u_1} → [inst : Monoid M] → (u : Mˣ) → (a b : M) → a * b = ↑u → Commute a b → Mˣ
Units.rightOfMul
#align add_units.right_of_add 
AddUnits.rightOfAdd: {M : Type u_1} → [inst : AddMonoid M] → (u : AddUnits M) → (a b : M) → a + b = ↑u → AddCommute a b → AddUnits M
AddUnits.rightOfAdd

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b → (IsAddUnit (a + b) ↔ IsAddUnit a ∧ IsAddUnit b)
to_additive]
theorem 
isUnit_mul_iff: ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b → (IsUnit (a * b) ↔ IsUnit a ∧ IsUnit b)
isUnit_mul_iff (
h: Commute a b
h : 
Commute: {S : Type ?u.13528} → [inst : Mul S] → S → S → Prop
Commute 
a: M
a 
b: M
b) : 
IsUnit: {M : Type ?u.13556} → [inst : Monoid M] → M → Prop
IsUnit (
a: M
a * 
b: M
b) ↔ 
IsUnit: {M : Type ?u.13618} → [inst : Monoid M] → M → Prop
IsUnit 
a: M
a ∧ 
IsUnit: {M : Type ?u.13621} → [inst : Monoid M] → M → Prop
IsUnit 
b: M
b :=
  ⟨fun ⟨
u: Mˣ
u, 
hu: ↑u = a * b
hu⟩ => ⟨(
u: Mˣ
u.
leftOfMul: {M : Type ?u.13675} → [inst : Monoid M] → (u : Mˣ) → (a b : M) → a * b = ↑u → Commute a b → Mˣ
leftOfMul 
a: M
a 
b: M
b 
hu: ↑u = a * b
hu.
symm: ∀ {α : Sort ?u.13688} {a b : α}, a = b → b = a
symm 
h: Commute a b
h).
isUnit: ∀ {M : Type ?u.13709} [inst : Monoid M] (u : Mˣ), IsUnit ↑u
isUnit, (
u: Mˣ
u.
rightOfMul: {M : Type ?u.13718} → [inst : Monoid M] → (u : Mˣ) → (a b : M) → a * b = ↑u → Commute a b → Mˣ
rightOfMul 
a: M
a 
b: M
b 
hu: ↑u = a * b
hu.
symm: ∀ {α : Sort ?u.13728} {a b : α}, a = b → b = a
symm 
h: Commute a b
h).
isUnit: ∀ {M : Type ?u.13736} [inst : Monoid M] (u : Mˣ), IsUnit ↑u
isUnit⟩,
  fun 
H: ?m.13809
H => 
H: ?m.13809
H.
1: ∀ {a b : Prop}, a ∧ b → a
1.
mul: ∀ {M : Type ?u.13815} [inst : Monoid M] {x y : M}, IsUnit x → IsUnit y → IsUnit (x * y)
mul 
H: ?m.13809
H.
2: ∀ {a b : Prop}, a ∧ b → b
2⟩
#align commute.is_unit_mul_iff 
Commute.isUnit_mul_iff: ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b → (IsUnit (a * b) ↔ IsUnit a ∧ IsUnit b)
Commute.isUnit_mul_iff
#align add_commute.is_add_unit_add_iff 
AddCommute.isAddUnit_add_iff: ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b → (IsAddUnit (a + b) ↔ IsAddUnit a ∧ IsAddUnit b)
AddCommute.isAddUnit_add_iff

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M}, IsAddUnit (a + a) ↔ IsAddUnit a
to_additive (attr := simp)]
theorem 
_root_.isUnit_mul_self_iff: IsUnit (a * a) ↔ IsUnit a
_root_.isUnit_mul_self_iff : 
IsUnit: {M : Type ?u.13958} → [inst : Monoid M] → M → Prop
IsUnit (
a: M
a * 
a: M
a) ↔ 
IsUnit: {M : Type ?u.14027} → [inst : Monoid M] → M → Prop
IsUnit 
a: M
a :=
  (
Commute.refl: ∀ {S : Type ?u.14031} [inst : Mul S] (a : S), Commute a a
Commute.refl 
a: M
a).
isUnit_mul_iff: ∀ {M : Type ?u.14053} [inst : Monoid M] {a b : M}, Commute a b → (IsUnit (a * b) ↔ IsUnit a ∧ IsUnit b)
isUnit_mul_iff.
trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans (
and_self_iff: ∀ (p : Prop), p ∧ p ↔ p
and_self_iff 
_: Prop
_)
  -- porting note: `and_self_iff` now has an implicit argument instead of an explicit one.
#align is_unit_mul_self_iff 
isUnit_mul_self_iff: ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsUnit (a * a) ↔ IsUnit a
isUnit_mul_self_iff
#align is_add_unit_add_self_iff 
isAddUnit_add_self_iff: ∀ {M : Type u_1} [inst : AddMonoid M] {a : M}, IsAddUnit (a + a) ↔ IsAddUnit a
isAddUnit_add_self_iff

end Monoid

section DivisionMonoid

variable [
DivisionMonoid: Type ?u.16707 → Type ?u.16707
DivisionMonoid 
G: Type ?u.14160
G] {
a: G
a 
b: G
b 
c: G
c 
d: G
d: 
G: Type ?u.14146
G}

@[
to_additive: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → AddCommute (-a) (-b)
to_additive]
protected theorem 
inv_inv: Commute a b → Commute a⁻¹ b⁻¹
inv_inv : 
Commute: {S : Type ?u.14175} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b → 
Commute: {S : Type ?u.14222} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a⁻¹ 
b: G
b⁻¹ :=
  
SemiconjBy.inv_inv_symm: ∀ {G : Type ?u.14273} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy a x y → SemiconjBy a⁻¹ y⁻¹ x⁻¹
SemiconjBy.inv_inv_symm
#align commute.inv_inv 
Commute.inv_inv: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b → Commute a⁻¹ b⁻¹
Commute.inv_inv
#align add_commute.neg_neg 
AddCommute.neg_neg: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → AddCommute (-a) (-b)
AddCommute.neg_neg

@[
to_additive: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute (-a) (-b) ↔ AddCommute a b
to_additive (attr := simp)]
theorem 
inv_inv_iff: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a⁻¹ b⁻¹ ↔ Commute a b
inv_inv_iff : 
Commute: {S : Type ?u.14339} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a⁻¹ 
b: G
b⁻¹ ↔ 
Commute: {S : Type ?u.14423} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b :=
  
SemiconjBy.inv_inv_symm_iff: ∀ {G : Type ?u.14427} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
SemiconjBy.inv_inv_symm_iff
#align commute.inv_inv_iff 
Commute.inv_inv_iff: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a⁻¹ b⁻¹ ↔ Commute a b
Commute.inv_inv_iff
#align add_commute.neg_neg_iff 
AddCommute.neg_neg_iff: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute (-a) (-b) ↔ AddCommute a b
AddCommute.neg_neg_iff

@[
to_additive: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → -(a + b) = -a + -b
to_additive]
protected theorem 
mul_inv: Commute a b → (a * b)⁻¹ = a⁻¹ * b⁻¹
mul_inv (
hab: Commute a b
hab : 
Commute: {S : Type ?u.14543} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b) : (
a: G
a * 
b: G
b)⁻¹ = 
a: G
a⁻¹ * 
b: G
b⁻¹ := by
Goals accomplished! 🐙 
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hab: Commute a b

(a * b)⁻¹ = a⁻¹ * b⁻¹rw [
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hab: Commute a b

(a * b)⁻¹ = a⁻¹ * b⁻¹
hab: Commute a b
hab.
eq: ∀ {S : Type ?u.14754} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq,
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hab: Commute a b

(b * a)⁻¹ = a⁻¹ * b⁻¹ 
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hab: Commute a b

(a * b)⁻¹ = a⁻¹ * b⁻¹
mul_inv_rev: ∀ {G : Type ?u.14815} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
mul_inv_rev
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hab: Commute a b

a⁻¹ * b⁻¹ = a⁻¹ * b⁻¹]
Goals accomplished! 🐙
#align commute.mul_inv 
Commute.mul_inv: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b → (a * b)⁻¹ = a⁻¹ * b⁻¹
Commute.mul_inv
#align add_commute.add_neg 
AddCommute.add_neg: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → -(a + b) = -a + -b
AddCommute.add_neg

@[
to_additive: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → -(a + b) = -a + -b
to_additive]
protected theorem 
inv: Commute a b → (a * b)⁻¹ = a⁻¹ * b⁻¹
inv (
hab: Commute a b
hab : 
Commute: {S : Type ?u.14898} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b) : (
a: G
a * 
b: G
b)⁻¹ = 
a: G
a⁻¹ * 
b: G
b⁻¹ := by
Goals accomplished! 🐙 
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hab: Commute a b

(a * b)⁻¹ = a⁻¹ * b⁻¹rw [
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hab: Commute a b

(a * b)⁻¹ = a⁻¹ * b⁻¹
hab: Commute a b
hab.
eq: ∀ {S : Type ?u.15109} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq,
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hab: Commute a b

(b * a)⁻¹ = a⁻¹ * b⁻¹ 
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hab: Commute a b

(a * b)⁻¹ = a⁻¹ * b⁻¹
mul_inv_rev: ∀ {G : Type ?u.15170} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
mul_inv_rev
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hab: Commute a b

a⁻¹ * b⁻¹ = a⁻¹ * b⁻¹]
Goals accomplished! 🐙
#align commute.inv 
Commute.inv: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b → (a * b)⁻¹ = a⁻¹ * b⁻¹
Commute.inv
#align add_commute.neg 
AddCommute.neg: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → -(a + b) = -a + -b
AddCommute.neg

@[
to_additive: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
  AddCommute b d → AddCommute (-b) c → a - b + (c - d) = a + c - (b + d)
to_additive]
protected theorem 
div_mul_div_comm: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
  Commute b d → Commute b⁻¹ c → a / b * (c / d) = a * c / (b * d)
div_mul_div_comm (
hbd: Commute b d
hbd : 
Commute: {S : Type ?u.15253} → [inst : Mul S] → S → S → Prop
Commute 
b: G
b 
d: G
d) (
hbc: Commute b⁻¹ c
hbc : 
Commute: {S : Type ?u.15301} → [inst : Mul S] → S → S → Prop
Commute 
b: G
b⁻¹ 
c: G
c) :
    
a: G
a / 
b: G
b * (
c: G
c / 
d: G
d) = 
a: G
a * 
c: G
c / (
b: G
b * 
d: G
d) := by
Goals accomplished! 🐙
  
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbd: Commute b d

hbc: Commute b⁻¹ c

a / b * (c / d) = a * c / (b * d)simp_rw [
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbd: Commute b d

hbc: Commute b⁻¹ c

a / b * (c / d) = a * c / (b * d)
div_eq_mul_inv: ∀ {G : Type ?u.15768} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
div_eq_mul_inv,
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbd: Commute b d

hbc: Commute b⁻¹ c

a * b⁻¹ * (c * d⁻¹) = a * c * (b * d)⁻¹ 
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbd: Commute b d

hbc: Commute b⁻¹ c

a / b * (c / d) = a * c / (b * d)
mul_inv_rev: ∀ {G : Type ?u.15867} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
mul_inv_rev,
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbd: Commute b d

hbc: Commute b⁻¹ c

a * b⁻¹ * (c * d⁻¹) = a * c * (d⁻¹ * b⁻¹) 
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbd: Commute b d

hbc: Commute b⁻¹ c

a / b * (c / d) = a * c / (b * d)
hbd: Commute b d
hbd.
inv_inv: ∀ {G : Type ?u.15920} [inst : DivisionMonoid G] {a b : G}, Commute a b → Commute a⁻¹ b⁻¹
inv_inv.
symm: ∀ {S : Type ?u.15931} [inst : Mul S] {a b : S}, Commute a b → Commute b a
symm.
eq: ∀ {S : Type ?u.15969} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq,
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbd: Commute b d

hbc: Commute b⁻¹ c

a * b⁻¹ * (c * d⁻¹) = a * c * (b⁻¹ * d⁻¹) 
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbd: Commute b d

hbc: Commute b⁻¹ c

a / b * (c / d) = a * c / (b * d)
hbc: Commute b⁻¹ c
hbc.
mul_mul_mul_comm: ∀ {S : Type ?u.16017} [inst : Semigroup S] {b c : S}, Commute b c → ∀ (a d : S), a * b * (c * d) = a * c * (b * d)
mul_mul_mul_comm
Goals accomplished! 🐙]
Goals accomplished! 🐙
#align commute.div_mul_div_comm 
Commute.div_mul_div_comm: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
  Commute b d → Commute b⁻¹ c → a / b * (c / d) = a * c / (b * d)
Commute.div_mul_div_comm
#align add_commute.sub_add_sub_comm 
AddCommute.sub_add_sub_comm: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
  AddCommute b d → AddCommute (-b) c → a - b + (c - d) = a + c - (b + d)
AddCommute.sub_add_sub_comm

@[
to_additive: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
  AddCommute c d → AddCommute b (-c) → a + b - (c + d) = a - c + (b - d)
to_additive]
protected theorem 
mul_div_mul_comm: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
  Commute c d → Commute b c⁻¹ → a * b / (c * d) = a / c * (b / d)
mul_div_mul_comm (
hcd: Commute c d
hcd : 
Commute: {S : Type ?u.16160} → [inst : Mul S] → S → S → Prop
Commute 
c: G
c 
d: G
d) (
hbc: Commute b c⁻¹
hbc : 
Commute: {S : Type ?u.16208} → [inst : Mul S] → S → S → Prop
Commute 
b: G
b 
c: G
c⁻¹) :
    
a: G
a * 
b: G
b / (
c: G
c * 
d: G
d) = 
a: G
a / 
c: G
c * (
b: G
b / 
d: G
d) :=
  (
hcd: Commute c d
hcd.
div_mul_div_comm: ∀ {G : Type ?u.16563} [inst : DivisionMonoid G] {a b c d : G},
  Commute b d → Commute b⁻¹ c → a / b * (c / d) = a * c / (b * d)
div_mul_div_comm 
hbc: Commute b c⁻¹
hbc.
symm: ∀ {S : Type ?u.16593} [inst : Mul S] {a b : S}, Commute a b → Commute b a
symm).
symm: ∀ {α : Sort ?u.16640} {a b : α}, a = b → b = a
symm
#align commute.mul_div_mul_comm 
Commute.mul_div_mul_comm: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
  Commute c d → Commute b c⁻¹ → a * b / (c * d) = a / c * (b / d)
Commute.mul_div_mul_comm
#align add_commute.add_sub_add_comm 
AddCommute.add_sub_add_comm: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
  AddCommute c d → AddCommute b (-c) → a + b - (c + d) = a - c + (b - d)
AddCommute.add_sub_add_comm

@[
to_additive: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
  AddCommute b c → AddCommute (-b) d → AddCommute (-c) d → a - b - (c - d) = a - c - (b - d)
to_additive]
protected theorem 
div_div_div_comm: Commute b c → Commute b⁻¹ d → Commute c⁻¹ d → a / b / (c / d) = a / c / (b / d)
div_div_div_comm (
hbc: Commute b c
hbc : 
Commute: {S : Type ?u.16718} → [inst : Mul S] → S → S → Prop
Commute 
b: G
b 
c: G
c) (
hbd: Commute b⁻¹ d
hbd : 
Commute: {S : Type ?u.16766} → [inst : Mul S] → S → S → Prop
Commute 
b: G
b⁻¹ 
d: G
d) (
hcd: Commute c⁻¹ d
hcd : 
Commute: {S : Type ?u.16806} → [inst : Mul S] → S → S → Prop
Commute 
c: G
c⁻¹ 
d: G
d) :
    
a: G
a / 
b: G
b / (
c: G
c / 
d: G
d) = 
a: G
a / 
c: G
c / (
b: G
b / 
d: G
d) := by
Goals accomplished! 🐙
  
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a / b / (c / d) = a / c / (b / d)simp_rw [
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a / b / (c / d) = a / c / (b / d)
div_eq_mul_inv: ∀ {G : Type ?u.17146} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
div_eq_mul_inv,
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a * b⁻¹ * (c * d⁻¹)⁻¹ = a * c⁻¹ * (b * d⁻¹)⁻¹ 
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a / b / (c / d) = a / c / (b / d)
mul_inv_rev: ∀ {G : Type ?u.17320} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
mul_inv_rev,
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a * b⁻¹ * (d⁻¹⁻¹ * c⁻¹) = a * c⁻¹ * (d⁻¹⁻¹ * b⁻¹) 
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a / b / (c / d) = a / c / (b / d)
inv_inv: ∀ {G : Type ?u.17384} [inst : InvolutiveInv G] (a : G), a⁻¹⁻¹ = a
inv_inv,
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a * b⁻¹ * (d * c⁻¹) = a * c⁻¹ * (d * b⁻¹) 
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a / b / (c / d) = a / c / (b / d)
hbd: Commute b⁻¹ d
hbd.
symm: ∀ {S : Type ?u.17430} [inst : Mul S] {a b : S}, Commute a b → Commute b a
symm.
eq: ∀ {S : Type ?u.17472} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq,
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a * b⁻¹ * (d * c⁻¹) = a * c⁻¹ * (b⁻¹ * d) 
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a / b / (c / d) = a / c / (b / d)
hcd: Commute c⁻¹ d
hcd.
symm: ∀ {S : Type ?u.17520} [inst : Mul S] {a b : S}, Commute a b → Commute b a
symm.
eq: ∀ {S : Type ?u.17562} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq,
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a * b⁻¹ * (c⁻¹ * d) = a * c⁻¹ * (b⁻¹ * d)
    
G: Type u_1

inst✝: DivisionMonoid G

a, b, c, d: G

hbc: Commute b c

hbd: Commute b⁻¹ d

hcd: Commute c⁻¹ d

a / b / (c / d) = a / c / (b / d)
hbc: Commute b c
hbc.
inv_inv: ∀ {G : Type ?u.17593} [inst : DivisionMonoid G] {a b : G}, Commute a b → Commute a⁻¹ b⁻¹
inv_inv.
mul_mul_mul_comm: ∀ {S : Type ?u.17604} [inst : Semigroup S] {b c : S}, Commute b c → ∀ (a d : S), a * b * (c * d) = a * c * (b * d)
mul_mul_mul_comm
Goals accomplished! 🐙]
Goals accomplished! 🐙
#align commute.div_div_div_comm 
Commute.div_div_div_comm: ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
  Commute b c → Commute b⁻¹ d → Commute c⁻¹ d → a / b / (c / d) = a / c / (b / d)
Commute.div_div_div_comm
#align add_commute.sub_sub_sub_comm 
AddCommute.sub_sub_sub_comm: ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
  AddCommute b c → AddCommute (-b) d → AddCommute (-c) d → a - b - (c - d) = a - c - (b - d)
AddCommute.sub_sub_sub_comm

end DivisionMonoid

section Group

variable [
Group: Type ?u.18444 → Type ?u.18444
Group 
G: Type ?u.17737
G] {
a: G
a 
b: G
b : 
G: Type ?u.17737
G}

@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → AddCommute a (-b)
to_additive]
theorem 
inv_right: Commute a b → Commute a b⁻¹
inv_right : 
Commute: {S : Type ?u.17758} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b → 
Commute: {S : Type ?u.17797} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b⁻¹ :=
  
SemiconjBy.inv_right: ∀ {G : Type ?u.17849} [inst : Group G] {a x y : G}, SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹
SemiconjBy.inv_right
#align commute.inv_right 
Commute.inv_right: ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → Commute a b⁻¹
Commute.inv_right
#align add_commute.neg_right 
AddCommute.neg_right: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → AddCommute a (-b)
AddCommute.neg_right

@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a (-b) ↔ AddCommute a b
to_additive (attr := simp)]
theorem 
inv_right_iff: Commute a b⁻¹ ↔ Commute a b
inv_right_iff : 
Commute: {S : Type ?u.17910} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b⁻¹ ↔ 
Commute: {S : Type ?u.17987} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b :=
  
SemiconjBy.inv_right_iff: ∀ {G : Type ?u.17991} [inst : Group G] {a x y : G}, SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
SemiconjBy.inv_right_iff
#align commute.inv_right_iff 
Commute.inv_right_iff: ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b⁻¹ ↔ Commute a b
Commute.inv_right_iff
#align add_commute.neg_right_iff 
AddCommute.neg_right_iff: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a (-b) ↔ AddCommute a b
AddCommute.neg_right_iff

@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → AddCommute (-a) b
to_additive]
theorem 
inv_left: Commute a b → Commute a⁻¹ b
inv_left : 
Commute: {S : Type ?u.18105} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b → 
Commute: {S : Type ?u.18144} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a⁻¹ 
b: G
b :=
  
SemiconjBy.inv_symm_left: ∀ {G : Type ?u.18196} [inst : Group G] {a x y : G}, SemiconjBy a x y → SemiconjBy a⁻¹ y x
SemiconjBy.inv_symm_left
#align commute.inv_left 
Commute.inv_left: ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → Commute a⁻¹ b
Commute.inv_left
#align add_commute.neg_left 
AddCommute.neg_left: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → AddCommute (-a) b
AddCommute.neg_left

@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute (-a) b ↔ AddCommute a b
to_additive (attr := simp)]
theorem 
inv_left_iff: ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a⁻¹ b ↔ Commute a b
inv_left_iff : 
Commute: {S : Type ?u.18257} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a⁻¹ 
b: G
b ↔ 
Commute: {S : Type ?u.18334} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b :=
  
SemiconjBy.inv_symm_left_iff: ∀ {G : Type ?u.18338} [inst : Group G] {a x y : G}, SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
SemiconjBy.inv_symm_left_iff
#align commute.inv_left_iff 
Commute.inv_left_iff: ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a⁻¹ b ↔ Commute a b
Commute.inv_left_iff
#align add_commute.neg_left_iff 
AddCommute.neg_left_iff: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute (-a) b ↔ AddCommute a b
AddCommute.neg_left_iff

@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → -a + b + a = b
to_additive]
protected theorem 
inv_mul_cancel: ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → a⁻¹ * b * a = b
inv_mul_cancel (
h: Commute a b
h : 
Commute: {S : Type ?u.18451} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b) : 
a: G
a⁻¹ * 
b: G
b * 
a: G
a = 
b: G
b := by
Goals accomplished! 🐙
  
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a⁻¹ * b * a = brw [
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a⁻¹ * b * a = b
h: Commute a b
h.
inv_left: ∀ {G : Type ?u.18642} [inst : Group G] {a b : G}, Commute a b → Commute a⁻¹ b
inv_left.
eq: ∀ {S : Type ?u.18659} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq,
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

b * a⁻¹ * a = b 
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a⁻¹ * b * a = b
inv_mul_cancel_right: ∀ {G : Type ?u.18714} [inst : Group G] (a b : G), a * b⁻¹ * b = a
inv_mul_cancel_right
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

b = b]
Goals accomplished! 🐙
#align commute.inv_mul_cancel 
Commute.inv_mul_cancel: ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → a⁻¹ * b * a = b
Commute.inv_mul_cancel
#align add_commute.neg_add_cancel 
AddCommute.neg_add_cancel: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → -a + b + a = b
AddCommute.neg_add_cancel

@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → -a + (b + a) = b
to_additive]
theorem 
inv_mul_cancel_assoc: ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → a⁻¹ * (b * a) = b
inv_mul_cancel_assoc (
h: Commute a b
h : 
Commute: {S : Type ?u.18780} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b) : 
a: G
a⁻¹ * (
b: G
b * 
a: G
a) = 
b: G
b := by
Goals accomplished! 🐙
  
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a⁻¹ * (b * a) = brw [
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a⁻¹ * (b * a) = b← 
mul_assoc: ∀ {G : Type ?u.18971} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc,
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a⁻¹ * b * a = b 
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a⁻¹ * (b * a) = b
h: Commute a b
h.
inv_mul_cancel: ∀ {G : Type ?u.19063} [inst : Group G] {a b : G}, Commute a b → a⁻¹ * b * a = b
inv_mul_cancel
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

b = b]
Goals accomplished! 🐙
#align commute.inv_mul_cancel_assoc 
Commute.inv_mul_cancel_assoc: ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → a⁻¹ * (b * a) = b
Commute.inv_mul_cancel_assoc
#align add_commute.neg_add_cancel_assoc 
AddCommute.neg_add_cancel_assoc: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → -a + (b + a) = b
AddCommute.neg_add_cancel_assoc

@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → a + b + -a = b
to_additive]
protected theorem 
mul_inv_cancel: Commute a b → a * b * a⁻¹ = b
mul_inv_cancel (
h: Commute a b
h : 
Commute: {S : Type ?u.19132} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b) : 
a: G
a * 
b: G
b * 
a: G
a⁻¹ = 
b: G
b := by
Goals accomplished! 🐙
  
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a * b * a⁻¹ = brw [
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a * b * a⁻¹ = b
h: Commute a b
h.
eq: ∀ {S : Type ?u.19323} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq,
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

b * a * a⁻¹ = b 
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a * b * a⁻¹ = b
mul_inv_cancel_right: ∀ {G : Type ?u.19376} [inst : Group G] (a b : G), a * b * b⁻¹ = a
mul_inv_cancel_right
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

b = b]
Goals accomplished! 🐙
#align commute.mul_inv_cancel 
Commute.mul_inv_cancel: ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → a * b * a⁻¹ = b
Commute.mul_inv_cancel
#align add_commute.add_neg_cancel 
AddCommute.add_neg_cancel: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → a + b + -a = b
AddCommute.add_neg_cancel

@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → a + (b + -a) = b
to_additive]
theorem 
mul_inv_cancel_assoc: Commute a b → a * (b * a⁻¹) = b
mul_inv_cancel_assoc (
h: Commute a b
h : 
Commute: {S : Type ?u.19450} → [inst : Mul S] → S → S → Prop
Commute 
a: G
a 
b: G
b) : 
a: G
a * (
b: G
b * 
a: G
a⁻¹) = 
b: G
b := by
Goals accomplished! 🐙
  
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a * (b * a⁻¹) = brw [
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a * (b * a⁻¹) = b← 
mul_assoc: ∀ {G : Type ?u.19641} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc,
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a * b * a⁻¹ = b 
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

a * (b * a⁻¹) = b
h: Commute a b
h.
mul_inv_cancel: ∀ {G : Type ?u.19733} [inst : Group G] {a b : G}, Commute a b → a * b * a⁻¹ = b
mul_inv_cancel
G: Type u_1

inst✝: Group G

a, b: G

h: Commute a b

b = b]
Goals accomplished! 🐙
#align commute.mul_inv_cancel_assoc 
Commute.mul_inv_cancel_assoc: ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → a * (b * a⁻¹) = b
Commute.mul_inv_cancel_assoc
#align add_commute.add_neg_cancel_assoc 
AddCommute.add_neg_cancel_assoc: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → a + (b + -a) = b
AddCommute.add_neg_cancel_assoc

end Group

end Commute

section CommGroup

variable [
CommGroup: Type ?u.20361 → Type ?u.20361
CommGroup 
G: Type ?u.19802
G] (
a: G
a 
b: G
b : 
G: Type ?u.19802
G)

@[
to_additive: ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + b + -a = b
to_additive (attr := simp)]
theorem 
mul_inv_cancel_comm: a * b * a⁻¹ = b
mul_inv_cancel_comm : 
a: G
a * 
b: G
b * 
a: G
a⁻¹ = 
b: G
b :=
  (
Commute.all: ∀ {S : Type ?u.19976} [inst : CommSemigroup S] (a b : S), Commute a b
Commute.all 
a: G
a 
b: G
b).
mul_inv_cancel: ∀ {G : Type ?u.19995} [inst : Group G] {a b : G}, Commute a b → a * b * a⁻¹ = b
mul_inv_cancel
#align mul_inv_cancel_comm 
mul_inv_cancel_comm: ∀ {G : Type u_1} [inst : CommGroup G] (a b : G), a * b * a⁻¹ = b
mul_inv_cancel_comm
#align add_neg_cancel_comm 
add_neg_cancel_comm: ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + b + -a = b
add_neg_cancel_comm

@[
to_additive: ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + (b + -a) = b
to_additive (attr := simp)]
theorem 
mul_inv_cancel_comm_assoc: a * (b * a⁻¹) = b
mul_inv_cancel_comm_assoc : 
a: G
a * (
b: G
b * 
a: G
a⁻¹) = 
b: G
b :=
  (
Commute.all: ∀ {S : Type ?u.20254} [inst : CommSemigroup S] (a b : S), Commute a b
Commute.all 
a: G
a 
b: G
b).
mul_inv_cancel_assoc: ∀ {G : Type ?u.20273} [inst : Group G] {a b : G}, Commute a b → a * (b * a⁻¹) = b
mul_inv_cancel_assoc
#align mul_inv_cancel_comm_assoc 
mul_inv_cancel_comm_assoc: ∀ {G : Type u_1} [inst : CommGroup G] (a b : G), a * (b * a⁻¹) = b
mul_inv_cancel_comm_assoc
#align add_neg_cancel_comm_assoc 
add_neg_cancel_comm_assoc: ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + (b + -a) = b
add_neg_cancel_comm_assoc

@[
to_additive: ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), -a + b + a = b
to_additive (attr := simp)]
theorem 
inv_mul_cancel_comm: a⁻¹ * b * a = b
inv_mul_cancel_comm : 
a: G
a⁻¹ * 
b: G
b * 
a: G
a = 
b: G
b :=
  (
Commute.all: ∀ {S : Type ?u.20532} [inst : CommSemigroup S] (a b : S), Commute a b
Commute.all 
a: G
a 
b: G
b).
inv_mul_cancel: ∀ {G : Type ?u.20551} [inst : Group G] {a b : G}, Commute a b → a⁻¹ * b * a = b
inv_mul_cancel
#align inv_mul_cancel_comm 
inv_mul_cancel_comm: ∀ {G : Type u_1} [inst : CommGroup G] (a b : G), a⁻¹ * b * a = b
inv_mul_cancel_comm
#align neg_add_cancel_comm 
neg_add_cancel_comm: ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), -a + b + a = b
neg_add_cancel_comm

@[
to_additive: ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), -a + (b + a) = b
to_additive (attr := simp)]
theorem 
inv_mul_cancel_comm_assoc: a⁻¹ * (b * a) = b
inv_mul_cancel_comm_assoc : 
a: G
a⁻¹ * (
b: G
b * 
a: G
a) = 
b: G
b :=
  (
Commute.all: ∀ {S : Type ?u.20810} [inst : CommSemigroup S] (a b : S), Commute a b
Commute.all 
a: G
a 
b: G
b).
inv_mul_cancel_assoc: ∀ {G : Type ?u.20829} [inst : Group G] {a b : G}, Commute a b → a⁻¹ * (b * a) = b
inv_mul_cancel_assoc
#align inv_mul_cancel_comm_assoc 
inv_mul_cancel_comm_assoc: ∀ {G : Type u_1} [inst : CommGroup G] (a b : G), a⁻¹ * (b * a) = b
inv_mul_cancel_comm_assoc
#align neg_add_cancel_comm_assoc 
neg_add_cancel_comm_assoc: ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), -a + (b + a) = b
neg_add_cancel_comm_assoc

end CommGroup