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