simp only [Function.updateITE]
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ updateITE f a b hd = f hd ∧ List.map (updateITE f a b) tl = List.map f tl
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ (if hd = a then b else f hd) = f hd ∧ List.map (updateITE f a b) tl = List.map f tl