rewrite [Array.getElem_append_left _ _ ((Array.size_map _ _).symm ▸ this)]
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
this : i < Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    Fin.castAdd m x.val[i]
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
this : i < Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val)[i] = Fin.castAdd m x.val[i]