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

State before:
α : Type ?u.84708
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.85382
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 : ∀ (y : β), CDifferentiable R fun x => f x y
⊢ (cderiv R fun x => ∫' y, f x y ∂μ) = fun x dx => ∫' y, cderiv R (fun x => f x y) x dx ∂μ
Tactic:
have := hf
State after:
α : Type ?u.84708
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.85382
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 this : ∀ (y : β), CDifferentiable R fun x => f x y
⊢ (cderiv R fun x => ∫' y, f x y ∂μ) = fun x dx => ∫' y, cderiv R (fun x => f x y) x dx ∂μ

State before:
α : Type ?u.84708
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.85382
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 this : ∀ (y : β), CDifferentiable R fun x => f x y
⊢ (cderiv R fun x => ∫' y, f x y ∂μ) = fun x dx => ∫' y, cderiv R (fun x => f x y) x dx ∂μ
Tactic:
sorry_proof
State after:
no goals