Theorem: Permutation.mul_assoc (Fifteen/Data/Permutation/Basic.lean)

State before:
n : Nat
x y z : Permutation n
i : Nat
hi : i < n
⊢ (x * y * z)[i] = (x * (y * z))[i]
Tactic:
simp only [get_mul]
State after:
no goals