Theorem: SciLean.Prob.FDistribution.bind.arg_xf.distribFwdDeriv_rule (SciLean/Modules/Prob/DistribDeriv/DistribFwdDeriv.lean)

State before:
W : Type u_1
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_1
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
g : X → Distribution Y
f : X → Y → Distribution Z
φ : Z → W × W
x dx : X
hg : DistribDifferentiable g
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
⊢ ⟪distribFwdDeriv (fun x' => g x' >>= f x') x dx, φ⟫ =
    ⟪distribFwdDeriv g x dx, fun y => ⟪distribFwdDeriv (fun x => f x y) x dx, φ⟫⟫
Tactic:
simp (disch := assumption)
  [distribFwdDeriv, fdaction_mk_apply, action_bind,
   Bind.bind.arg_xf.distribDeriv_rule, Prod.mk.injEq, true_and, add_assoc]
State after:
W : Type u_1
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_1
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
g : X → Distribution Y
f : X → Y → Distribution Z
φ : Z → W × W
x dx : X
hg : DistribDifferentiable g
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
⊢ ⟪g x, fun x' => ⟪distribDeriv (fun x => f x x') x dx, fun x => (φ x).1⟫⟫ +
      ⟪g x, fun x' => ⟪f x x', fun x => (φ x).2⟫⟫ =
    ⟪g x, fun x_1 => ⟪distribDeriv (fun x => f x x_1) x dx, fun x => (φ x).1⟫ + ⟪f x x_1, fun x => (φ x).2⟫⟫

State before:
W : Type u_1
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_1
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
g : X → Distribution Y
f : X → Y → Distribution Z
φ : Z → W × W
x dx : X
hg : DistribDifferentiable g
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
⊢ ⟪g x, fun x' => ⟪distribDeriv (fun x => f x x') x dx, fun x => (φ x).1⟫⟫ +
      ⟪g x, fun x' => ⟪f x x', fun x => (φ x).2⟫⟫ =
    ⟪g x, fun x_1 => ⟪distribDeriv (fun x => f x x_1) x dx, fun x => (φ x).1⟫ + ⟪f x x_1, fun x => (φ x).2⟫⟫
Tactic:
sorry
State after:
no goals