no goals
α : Type u_1
β : Type ?u.300214
γ : Type ?u.300217
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
i : α
p : δ i → Prop
hf : p (f i)
hg : p (g i)
⊢ p (piecewise s f g i)
by_cases hi : i ∈ s <;> simpa [hi]