simp only [Finset.mem_image]
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ f y ∈ image (Function.updateITE f x x) S
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ ∃ a ∈ S, Function.updateITE f x x a = f y