no goals
α : Type u_1
β : Type ?u.302885
γ : Type ?u.302888
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
⊢ piecewise {i} f g = update g i (f i)
rw [← insert_emptyc_eq, piecewise_insert, piecewise_empty]