[GOAL]
S : Type u_1
inst✝ : Semigroup S
a b x y z x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x') (y * y')
[PROOFSTEP]
unfold SemiconjBy
[GOAL]
S : Type u_1
inst✝ : Semigroup S
a b x y z x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ a * (x * x') = y * y' * a
[PROOFSTEP]
rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]
[GOAL]
S : Type u_1
inst✝ : Semigroup S
a b x y z x' y' : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ SemiconjBy (a * b) x z
[PROOFSTEP]
unfold SemiconjBy
[GOAL]
S : Type u_1
inst✝ : Semigroup S
a b x y z x' y' : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ a * b * x = z * (a * b)
[PROOFSTEP]
rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]
[GOAL]
M : Type u_1
inst✝ : MulOneClass M
a : M
⊢ SemiconjBy a 1 1
[PROOFSTEP]
rw [SemiconjBy, mul_one, one_mul]
[GOAL]
M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ a * ↑x⁻¹ = ↑y⁻¹ * (↑y * a) * ↑x⁻¹
[PROOFSTEP]
rw [Units.inv_mul_cancel_left]
[GOAL]
M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ ↑y⁻¹ * (↑y * a) * ↑x⁻¹ = ↑y⁻¹ * a
[PROOFSTEP]
rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]
[GOAL]
M : Type u_1
inst✝ : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a) x y
⊢ ↑a⁻¹ * y = ↑a⁻¹ * (y * ↑a * ↑a⁻¹)
[PROOFSTEP]
rw [Units.mul_inv_cancel_right]
[GOAL]
M : Type u_1
inst✝ : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a) x y
⊢ ↑a⁻¹ * (y * ↑a * ↑a⁻¹) = x * ↑a⁻¹
[PROOFSTEP]
rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left]
[GOAL]
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ n) (y ^ n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a (x ^ Nat.zero) (y ^ Nat.zero)
[PROOFSTEP]
rw [pow_zero, pow_zero]
[GOAL]
case zero
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1
[PROOFSTEP]
exact SemiconjBy.one_right _
[GOAL]
case succ
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ Nat.succ n) (y ^ Nat.succ n)
[PROOFSTEP]
rw [pow_succ, pow_succ]
[GOAL]
case succ
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x * x ^ n) (y * y ^ n)
[PROOFSTEP]
exact h.mul_right ih
[GOAL]
G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ (a⁻¹ * x⁻¹)⁻¹ = (y⁻¹ * a⁻¹)⁻¹ ↔ SemiconjBy a y x
[PROOFSTEP]
rw [mul_inv_rev, mul_inv_rev, inv_inv, inv_inv, inv_inv, eq_comm, SemiconjBy]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ x✝ y a x : G
⊢ SemiconjBy a x (a * x * a⁻¹)
[PROOFSTEP]
unfold SemiconjBy
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ x✝ y a x : G
⊢ a * x = a * x * a⁻¹ * a
[PROOFSTEP]
rw [mul_assoc, inv_mul_self, mul_one]
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoid M
a x y : M
h : x = y
⊢ SemiconjBy a x y
[PROOFSTEP]
rw [h, SemiconjBy, mul_comm]
[GOAL]
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)
[PROOFSTEP]
unfold SemiconjBy
[GOAL]
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ ↑u * x = ↑u * x * ↑u⁻¹ * ↑u
[PROOFSTEP]
rw [Units.inv_mul_cancel_right]
