if h : i < n then
  rewrite [dif_pos h]; exact x.get_castAdd_lt m i h
else
  rewrite [dif_neg h]; exact x.get_castAdd_ge m i (Nat.le_of_not_lt h)
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
⊢ (castAdd m x)[i] = if h : i < n then Fin.castAdd m x[i] else { val := i, isLt := hi }
no goals