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

State before:
c : Prop
inst✝ : Decidable c
x y : ENNReal
⊢ (if c then x else y).toReal = if c then x.toReal else y.toReal
Tactic:
sorry_proof
State after:
no goals