no goals
α : Type u_1
β : Type u_2
ι : Type ?u.16343
M : Type u_3
N : Type ?u.16349
inst✝² : One M
inst✝¹ : One N
s✝ t : Set α
f✝ g : α → M
a : α
h : M → β
f : α → M
s : Set α
x : α
inst✝ : DecidablePred fun x => x ∈ s
this : DecidablePred fun x => x ∈ s := Classical.decPred fun x => x ∈ s
⊢ h (mulIndicator s f x) = piecewise s (h ∘ f) (const α (h 1)) x
convert s.apply_piecewise f (const α 1) (fun _ => h) (x := x) using 2