Theorem: SciLean.Prob.distribFwdDeriv_const (SciLean/Modules/Prob/DistribDeriv/DistribFwdDeriv.lean)

State before:
W : Type ?u.22303
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.23178
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.23613
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (distribFwdDeriv fun x => a) = fun w _dw => { val := a, dval := 0 }
Tactic:
unfold distribFwdDeriv
State after:
W : Type ?u.22303
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.23178
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.23613
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx => { val := (fun x => a) x, dval := distribDeriv (fun x => a) x dx }) = fun w _dw => { val := a, dval := 0 }

State before:
W : Type ?u.22303
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.23178
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.23613
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx => { val := (fun x => a) x, dval := distribDeriv (fun x => a) x dx }) = fun w _dw => { val := a, dval := 0 }
Tactic:
simp
State after:
no goals