no goals
α : Type u_1
β : Type ?u.72650
γ : Type ?u.72653
ι : Sort ?u.72656
π : α → Type ?u.72661
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ piecewise (insert j s) f g j = f j
simp [piecewise]