have : i ≥ x.val.size := x.size_eq.symm ▸ h
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    { val := i, isLt := hi }
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] =
    { val := i, isLt := hi }