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

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