Theorem: SciLean.split_integral_over_set_of_ite (SciLean/Core/Integral/CIntegral.lean)

State before:
R : Type u_3
inst✝⁶ : RealScalar R
inst✝⁵ : DecidableRel fun x x_1 => x ≤ x_1
X : Type u_1
inst✝⁴ : MeasureSpace X
Y : Type u_2
inst✝³ : AddCommGroup Y
inst✝² : _root_.Module ℝ Y
Z : Type ?u.77184
inst✝¹ : AddCommGroup Z
inst✝ : _root_.Module ℝ Z
φ ψ : X → R
f g : X → Y
A : Set X
⊢ ∫' x, if ψ x ≤ φ x then f x else g x ∂volume.restrict A =
    ∫' x, f x ∂volume.restrict ({x' | 0 ≤ φ x' - ψ x'} ∩ A) + ∫' x, g x ∂volume.restrict ({x' | 0 ≤ ψ x' - φ x'} ∩ A)
Tactic:
sorry_proof
State after:
no goals