no goals
α : Type u_1
β : Type u_2
γ : Type ?u.4394524
δ : Type ?u.4394527
ι : Type ?u.4394530
R : Type ?u.4394533
R' : Type ?u.4394536
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f g : α → β
hst : s =ᶠ[ae μ] t
x : α
hx : x ∈ s ↔ x ∈ t
⊢ piecewise s f g x = piecewise t f g x
simp [piecewise, hx]