apply Finset.image_congr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
⊢ image (Function.updateITE f x x') (S \ {x}) = image f (S \ {x})
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
⊢ Set.EqOn (Function.updateITE f x x') f ↑(S \ {x})