simp only [Function.updateITE]
case h
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
⊢ updateITE f a (g a) x = g x
case h
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
⊢ (if x = a then g a else f x) = g x