Theorem: SciLean.Scalar.ofReal_dite (SciLean/Core/Objects/Scalar.lean)

State before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → ℝ
e : ¬c → ℝ
⊢ ofReal R (if h : c then t h else e h) = if h : c then ofReal R (t h) else ofReal R (e h)
Tactic:
if h : c then simp[h] else simp[h]
State after:
no goals

State before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → ℝ
e : ¬c → ℝ
h : c
⊢ ofReal R (if h : c then t h else e h) = if h : c then ofReal R (t h) else ofReal R (e h)
Tactic:
simp[h]
State after:
no goals

State before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → ℝ
e : ¬c → ℝ
h : ¬c
⊢ ofReal R (if h : c then t h else e h) = if h : c then ofReal R (t h) else ofReal R (e h)
Tactic:
simp[h]
State after:
no goals