no goals
α : Type u_1
β : Type ?u.296498
γ : Type ?u.296501
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
i : α
hi : ¬i ∈ s
⊢ piecewise s f g i = g i
simp [piecewise, hi]