Simp "if_then_else" in a Vector.map with assumption

Stream: lean4

[Anton Mueller]

ts : Vector Var m
h_all : ∀ t ∈ ts, t ∈ pdom
h_in_xs : List.Mem (w, pred n m ts) xs
⊢ (↑(f w), pred n m (Vector.map (fun t ↦ ↑t) (Vector.map (fun x_1 ↦ if h : x_1 ∈ pdom then ⟨x_1, h⟩ else default) ts))) ∈ xs

The above is the goal i have to prove. I also know how, once the inner Vector.map is reduced. In the presence of the assumption h_in_xs the if-then-else always reduces to the then part, so it should become the following:

⊢ (↑(f w), pred n m (Vector.map (fun t ↦ ↑t) (Vector.map (fun x_1 ↦  ⟨x_1, h⟩) ts))) ∈ xs

Is there a useful thoerem, something like "map_iteFun_allIf_is_mapThen" or a nice tactic?

Thank you!

[Kim Morrison]

Can you produce an #mwe?

[Aaron Liu]

Why have you unfolded to List.Mem?