R✝ : Type ?u.30897
inst✝¹ : Rack R✝
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
R✝ : Type ?u.30897
inst✝¹ : Rack R✝
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
rw [self_distrib]
no goals
R✝ : Type ?u.30897
inst✝¹ : Rack R✝
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
rw [left_cancel]