no goals
α : Type u_2
β : Type ?u.90308
γ : Type ?u.90311
ι : Sort ?u.90314
π : α → Type ?u.90319
δ : α → Sort u_3
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_1
h : (i : α) → δ i → δ' i
x : α
⊢ h x (piecewise s f g x) = piecewise s (fun x => h x (f x)) (fun x => h x (g x)) x
by_cases hx : x ∈ s <;> simp [hx]