-- Mathlib/Analysis/Calculus/ParametricIntegral.lean
theorem hasDerivAt_integral_of_dominated_loc_of_deriv_le (ε_pos : 0 < ε)
    (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ) (hF_int : Integrable (F x₀) μ)
    {F' : 𝕜 → α → E} (hF'_meas : AEStronglyMeasurable (F' x₀) μ)
    (h_bound : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a) (bound_integrable : Integrable bound μ)
    (h_diff : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (F · a) (F' x a) x) :
    Integrable (F' x₀) μ ∧ HasDerivAt (fun n ↦ ∫ a, F n a ∂μ) (∫ a, F' x₀ a ∂μ) x₀

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₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' x₀ a) x₀
this : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)
⊢ Integrable (F' x₀) μ ∧ HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀

Tactic:
exact
  hasDerivAt_integral_of_dominated_loc_of_lip ε_pos hF_meas hF_int hF'_meas this bound_integrable
    diff_x₀

Result:
no goals

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₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x
ha_bound : ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a
x : 𝕜
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖ ≤ |bound a|

Tactic:
exact (ha_bound x x_in).trans (le_abs_self _)

Result:
no goals

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₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x
ha_bound : ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a
⊢ LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)

Tactic:
refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasDerivWithin_le
  (fun x x_in ↦ (ha_deriv x x_in).hasDerivWithinAt) fun x x_in ↦ ?_

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₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x
ha_bound : ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a
x : 𝕜
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖₊ ≤ Real.nnabs (bound a)

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₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x
⊢ Integrable (F' x₀) μ ∧ HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀

Tactic:
have x₀_in : x₀ ∈ ball x₀ ε := mem_ball_self ε_pos

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₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x
x₀_in : x₀ ∈ ball x₀ ε
⊢ Integrable (F' x₀) μ ∧ HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀

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₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' x₀ a) x₀
⊢ Integrable (F' x₀) μ ∧ HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀

Tactic:
have : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x : 𝕜 ↦ F x a) (ball x₀ ε) := by
  apply (h_diff.and h_bound).mono
  rintro a ⟨ha_deriv, ha_bound⟩
  refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasDerivWithin_le
    (fun x x_in ↦ (ha_deriv x x_in).hasDerivWithinAt) fun x x_in ↦ ?_
  rw [← NNReal.coe_le_coe, coe_nnnorm, Real.coe_nnabs]
  exact (ha_bound x x_in).trans (le_abs_self _)

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₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' x₀ a) x₀
this : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)
⊢ Integrable (F' x₀) μ ∧ HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀