simp only [Function.updateITE]
case right
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ Function.updateITE f x x y = f y
case right
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ (if y = x then x else f y) = f y