R : Type u_1
inst✝ : Rack R
x y z : R
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z
rw [← left_cancel (x ◃⁻¹ y), right_inv, ← left_cancel x, right_inv, self_distrib]
no goals
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
repeat' rw [right_inv]
no goals
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ y ◃ y ◃⁻¹ z = z
rw [right_inv]