Theorem: SciLean.Prob.distribDeriv_const (SciLean/Modules/Prob/DistribDeriv/DistribDeriv.lean)

State before:
W : Type ?u.3082
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.3535
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.3761
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (distribDeriv fun x => a) = fun w dw => 0
Tactic:
unfold distribDeriv
State after:
W : Type ?u.3082
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.3535
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.3761
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx =>
      {
        action := fun {Y} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] φ =>
          (fderiv ℝ (fun x => ⟪(fun x => a) x, φ⟫) x) dx }) =
    fun w dw => 0

State before:
W : Type ?u.3082
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.3535
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.3761
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx =>
      {
        action := fun {Y} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] φ =>
          (fderiv ℝ (fun x => ⟪(fun x => a) x, φ⟫) x) dx }) =
    fun w dw => 0
Tactic:
simp
State after:
W : Type ?u.3082
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.3535
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.3761
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx => { action := fun {Y} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] φ => 0 }) = fun w dw => 0

State before:
W : Type ?u.3082
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.3535
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.3761
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx => { action := fun {Y} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] φ => 0 }) = fun w dw => 0
Tactic:
rfl
State after:
no goals