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

State before:
n : Nat
x : Permutation n
i : Nat
hi : i < n
⊢ (x * 1)[i] = x[i]
Tactic:
rw [get_mul, get_one]
State after:
no goals