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

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

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