no goals
α : Type u_1
β : Type u_2
γ : Type ?u.88049
ι : Sort ?u.88052
π : α → Type ?u.88057
δ : α → Sort ?u.88062
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t t' : Set α
h : EqOn f g (t ∩ s)
h' : EqOn f' g (t' ∩ sᶜ)
⊢ EqOn (piecewise s f f') g (Set.ite s t t')
simp [eqOn_piecewise, *]