no goals
α : Type u_2
β : Type u_1
γ : Type ?u.89108
ι : Sort ?u.89111
π : α → Type ?u.89116
δ : α → Sort ?u.89121
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
⊢ x ∈ piecewise s f g ⁻¹' t ↔ x ∈ Set.ite s (f ⁻¹' t) (g ⁻¹' t)
by_cases x ∈ s <;> simp [*, Set.ite]