simp only [Function.updateITE]
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
a1 : a ∈ S ∧ ¬a = x
⊢ Function.updateITE f x x' a = f a
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
a1 : a ∈ S ∧ ¬a = x
⊢ (if a = x then x' else f a) = f a