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