[GOAL]
G : Type u_1
S : Type u_2
inst✝ : Semigroup S
a✝ b c : S
h : Commute b c
a : S
⊢ a * b * c = a * c * b
[PROOFSTEP]
simp only [mul_assoc, h.eq]
[GOAL]
G : Type u_1
S : Type u_2
inst✝ : Semigroup S
a b c✝ : S
h : Commute a b
c : S
⊢ a * (b * c) = b * (a * c)
[PROOFSTEP]
simp only [← mul_assoc, h.eq]
[GOAL]
G : Type u_1
S : Type u_2
inst✝ : Semigroup S
a✝ b c : S
hbc : Commute b c
a d : S
⊢ a * b * (c * d) = a * c * (b * d)
[PROOFSTEP]
simp only [hbc.left_comm, mul_assoc]
[GOAL]
G : Type u_1
M : Type u_2
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
[PROOFSTEP]
rw [← mul_assoc, hu, u.mul_inv]
[GOAL]
G : Type u_1
M : Type u_2
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 = 1
[PROOFSTEP]
have : Commute a u := hu ▸ (Commute.refl _).mul_right hc
[GOAL]
G : Type u_1
M : Type u_2
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
[PROOFSTEP]
rw [← this.units_inv_right.right_comm, ← hc.eq, hu, u.mul_inv]
[GOAL]
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hab : Commute a b
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
[PROOFSTEP]
rw [hab.eq, mul_inv_rev]
[GOAL]
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hab : Commute a b
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
[PROOFSTEP]
rw [hab.eq, mul_inv_rev]
[GOAL]
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)
[PROOFSTEP]
simp_rw [div_eq_mul_inv, mul_inv_rev, hbd.inv_inv.symm.eq, hbc.mul_mul_mul_comm]
[GOAL]
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)
[PROOFSTEP]
simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq, hbc.inv_inv.mul_mul_mul_comm]
[GOAL]
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * b * a = b
[PROOFSTEP]
rw [h.inv_left.eq, inv_mul_cancel_right]
[GOAL]
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * (b * a) = b
[PROOFSTEP]
rw [← mul_assoc, h.inv_mul_cancel]
[GOAL]
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a * b * a⁻¹ = b
[PROOFSTEP]
rw [h.eq, mul_inv_cancel_right]
[GOAL]
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a * (b * a⁻¹) = b
[PROOFSTEP]
rw [← mul_assoc, h.mul_inv_cancel]