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

State before:
W : Type u_1
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.9959
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.10394
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
val dval : Distribution X
φ : X → W × W
⊢ ⟪{ val := val, dval := dval }, φ⟫ = (⟪val, fun x => (φ x).1⟫, ⟪dval, fun x => (φ x).1⟫ + ⟪val, fun x => (φ x).2⟫)
Tactic:
rfl
State after:
no goals