no goals
α✝ : Type ?u.98315
β : Type ?u.98318
γ : Type ?u.98321
ι✝ : Sort ?u.98324
π : α✝ → Type ?u.98329
δ : α✝ → Sort ?u.98334
s✝ : Set α✝
f g : (i : α✝) → δ i
inst✝¹ : (j : α✝) → Decidable (j ∈ s✝)
ι : Type u_1
α : ι → Type u_2
s : Set ι
t t' : (i : ι) → Set (α i)
inst✝ : (x : ι) → Decidable (x ∈ s)
⊢ pi univ (piecewise s t t') = pi s t ∩ pi (sᶜ) t'
simp [compl_eq_univ_diff]