no goals
α : Type u_1
β : Type ?u.82701
γ : Type ?u.82704
ι : Sort ?u.82707
π : α → Type ?u.82712
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
i j : α
h : i ≠ j
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ piecewise (insert j s) f g i = piecewise s f g i
simp [piecewise, h]