I'm not sure why you want this, since you explicitly defined x to have type Fin (4 + 2), so why would you want Lean to tell you differently?

One thing you could do is the following:

#simp type_of% x -- Fin 6

Here type_of% e is a special elaborator that gives you the type of term e, and the #simp command simplifies a particular expression (in the same way that the simp tactic would).