α : Type ?u.2687
M₀ : Type ?u.2690
G₀ : Type u_1
M₀' : Type ?u.2696
G₀' : Type ?u.2699
F : Type ?u.2702
F' : Type ?u.2705
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)
α : Type ?u.2687
M₀ : Type ?u.2690
G₀ : Type u_1
M₀' : Type ?u.2696
G₀' : Type ?u.2699
F : Type ?u.2702
F' : Type ?u.2705
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x / x') (y / y')
rw [div_eq_mul_inv, div_eq_mul_inv]
no goals
α : Type ?u.2687
M₀ : Type ?u.2690
G₀ : Type u_1
M₀' : Type ?u.2696
G₀' : Type ?u.2699
F : Type ?u.2702
F' : Type ?u.2705
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)
exact h.mul_right h'.inv_right₀