English
For all x,y,z in the rack, x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z, i.e., inverse action distributes with respect to itself.
Русский
Для всех x,y,z в раке верно x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z, то есть обратное действие самораспределимо.
LaTeX
$$$x \triangleleft^{-1} y \triangleleft^{-1} z = (x \triangleleft^{-1} y) \triangleleft^{-1} x \triangleleft^{-1} z$$$
Lean4
theorem self_distrib_inv {x y z : R} : x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z :=
by
rw [← left_cancel (x ◃⁻¹ y), right_inv, ← left_cancel x, right_inv, self_distrib]
repeat' rw [right_inv]