no goals
α : Type u_2
β : Type ?u.23061
γ : Type ?u.23064
inst✝¹ : Fintype α
s t : Finset α
δ : α → Sort u_1
inst✝ : DecidableEq α
a : α
f g : (a : α) → δ a
⊢ piecewise (erase univ a) f g = update f a (g a)
rw [← compl_singleton, piecewise_compl, piecewise_singleton]