Theorem: SciLean.cintegral.arg_f.fwdDeriv_rule (SciLean/Core/Integral/CIntegral.lean)

State before:
α : Type ?u.87292
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.87966
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf : ∀ (x : β), CDifferentiable R fun x_1 => f x_1 x
⊢ (fwdDeriv R fun x => ∫' y, f x y ∂μ) = fun x dx => ∫' y, fwdDeriv R (fun x => f x y) x dx ∂μ
Tactic:
unfold fwdDeriv
State after:
α : Type ?u.87292
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.87966
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf : ∀ (x : β), CDifferentiable R fun x_1 => f x_1 x
⊢ (fun x dx => ((fun x => ∫' y, f x y ∂μ) x, cderiv R (fun x => ∫' y, f x y ∂μ) x dx)) = fun x dx =>
    ∫' y, ((fun x => f x y) x, cderiv R (fun x => f x y) x dx) ∂μ

State before:
α : Type ?u.87292
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.87966
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf : ∀ (x : β), CDifferentiable R fun x_1 => f x_1 x
⊢ (fun x dx => ((fun x => ∫' y, f x y ∂μ) x, cderiv R (fun x => ∫' y, f x y ∂μ) x dx)) = fun x dx =>
    ∫' y, ((fun x => f x y) x, cderiv R (fun x => f x y) x dx) ∂μ
Tactic:
fun_trans [cintegral_prod_mk]
State after:
no goals