α : Type u_2
β : Type u_1
ι : Type ?u.1469486
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
⊢ (∫⁻ (b : β) in t, g b ∂if a ∈ s then ↑κ a else ↑η a) =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂↑κ a else ∫⁻ (b : β) in t, g b ∂↑η a
α : Type u_2
β : Type u_1
ι : Type ?u.1469486
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
⊢ (∫⁻ (b : β) in t, g b ∂↑(piecewise hs κ η) a) =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂↑κ a else ∫⁻ (b : β) in t, g b ∂↑η a
simp_rw [piecewise_apply]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.1469486
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
⊢ (∫⁻ (b : β) in t, g b ∂if a ∈ s then ↑κ a else ↑η a) =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂↑κ a else ∫⁻ (b : β) in t, g b ∂↑η a
split_ifs <;> rfl