-- Mathlib/Analysis/Calculus/ParametricIntegral.lean
theorem hasDerivAt_integral_of_dominated_loc_of_lip {F' : α → E} (ε_pos : 0 < ε)
    (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ) (hF_int : Integrable (F x₀) μ)
    (hF'_meas : AEStronglyMeasurable F' μ)
    (h_lipsch : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs <| bound a) (F · a) (ball x₀ ε))
    (bound_integrable : Integrable (bound : α → ℝ) μ)
    (h_diff : ∀ᵐ a ∂μ, HasDerivAt (F · a) (F' a) x₀) :
    Integrable F' μ ∧ HasDerivAt (fun x ↦ ∫ a, F x a ∂μ) (∫ a, F' a ∂μ) x₀

Proof state:
case intro
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
ε : ℝ
F : 𝕜 → α → E
x₀ : 𝕜
F' : α → E
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
key : HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
⊢ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
by_cases hE : CompleteSpace E

Result:
case pos
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
ε : ℝ
F : 𝕜 → α → E
x₀ : 𝕜
F' : α → E
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
key : HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
hE : CompleteSpace E
⊢ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

case neg
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
ε : ℝ
F : 𝕜 → α → E
x₀ : 𝕜
F' : α → E
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
key : HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
hE : ¬CompleteSpace E
⊢ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Proof state:
case neg
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
ε : ℝ
F : 𝕜 → α → E
x₀ : 𝕜
F' : α → E
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
key : HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
hE : ¬CompleteSpace E
⊢ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
simpa [integral, hE] using hasDerivAt_const x₀ 0

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
ε : ℝ
F : 𝕜 → α → E
x₀ : 𝕜
F' : α → E
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
hF'_int : Integrable (⇑L ∘ F') μ
key : HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
⊢ Integrable F' μ

Tactic:
rw [← integrable_norm_iff hm] at hF'_int

Result:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
ε : ℝ
F : 𝕜 → α → E
x₀ : 𝕜
F' : α → E
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
hF'_int : Integrable (fun a => ‖(⇑L ∘ F') a‖) μ
key : HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
⊢ Integrable F' μ

Proof state:
case intro
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
ε : ℝ
F : 𝕜 → α → E
x₀ : 𝕜
F' : α → E
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
key : HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
⊢ Integrable F' μ ∧ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
refine ⟨hF'_int, ?_⟩

Result:
case intro
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
ε : ℝ
F : 𝕜 → α → E
x₀ : 𝕜
F' : α → E
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
key : HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
⊢ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀