simp only [Array.size_map, Fin.addNat_mk, Fin.cast_mk, x.size_eq]
case a
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ ↑(Fin.cast (_ : m + n = n + m)
        (Fin.addNat
          { val := i - Array.size (Array.map (Fin.castAdd m) x.val),
            isLt := (_ : i - Array.size (Array.map (Fin.castAdd m) x.val) < m) }
          n)) =
    ↑{ val := i, isLt := hi }
case a
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ i - n + n = i