Theorem: SciLean.ite_pull_measureOf (SciLean/Core/Integral/Common.lean)

State before:
X : Type u_1
inst✝¹ : MeasurableSpace X
c : Prop
inst✝ : Decidable c
μ ν : Measure X
A : Set X
⊢ ↑↑(if c then μ else ν) A = if c then ↑↑μ A else ↑↑ν A
Tactic:
sorry_proof
State after:
no goals