Theorem: SciLean.ite_apply (SciLean/Core/Distribution/BungeeTest.lean)

State before:
R : Type ?u.110294
inst✝⁶ : RealScalar R
W : Type ?u.110300
inst✝⁵ : SemiHilbert R W
X : Type ?u.110330
inst✝⁴ : SemiHilbert R X
Y : Type ?u.110354
inst✝³ : SemiHilbert R Y
Z : Type ?u.110378
inst✝² : SemiHilbert R Z
inst✝¹ : MeasureSpace R
m l₁ l₂ k₁ k₂ α✝ height : R
α : Type u_1
β : Type u_2
c : Prop
inst✝ : Decidable c
t e : α → β
x : α
⊢ (if c then t else e) x = if c then t x else e x
Tactic:
if h : c then simp[h] else simp[h]
State after:
no goals

State before:
R : Type ?u.110294
inst✝⁶ : RealScalar R
W : Type ?u.110300
inst✝⁵ : SemiHilbert R W
X : Type ?u.110330
inst✝⁴ : SemiHilbert R X
Y : Type ?u.110354
inst✝³ : SemiHilbert R Y
Z : Type ?u.110378
inst✝² : SemiHilbert R Z
inst✝¹ : MeasureSpace R
m l₁ l₂ k₁ k₂ α✝ height : R
α : Type u_1
β : Type u_2
c : Prop
inst✝ : Decidable c
t e : α → β
x : α
h : c
⊢ (if c then t else e) x = if c then t x else e x
Tactic:
simp[h]
State after:
no goals

State before:
R : Type ?u.110294
inst✝⁶ : RealScalar R
W : Type ?u.110300
inst✝⁵ : SemiHilbert R W
X : Type ?u.110330
inst✝⁴ : SemiHilbert R X
Y : Type ?u.110354
inst✝³ : SemiHilbert R Y
Z : Type ?u.110378
inst✝² : SemiHilbert R Z
inst✝¹ : MeasureSpace R
m l₁ l₂ k₁ k₂ α✝ height : R
α : Type u_1
β : Type u_2
c : Prop
inst✝ : Decidable c
t e : α → β
x : α
h : ¬c
⊢ (if c then t else e) x = if c then t x else e x
Tactic:
simp[h]
State after:
no goals