if h : c then simp[h] else simp[h]
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → ENNReal
e : ¬c → ENNReal
⊢ ↑(if h : c then t h else e h) = if h : c then ↑(t h) else ↑(e h)
no goals