simp[h]
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
no goals