awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : H → α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' x a) x
this : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' x₀ a) x₀
⊢ ∀ᵐ (a : α) ∂μ,
    LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : H) ↦ F x a) (ball x₀ ε)

Tactic:
have : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (F · a) (ball x₀ ε) := by
    apply (h_diff.and h_bound).mono
    rintro a ⟨ha_deriv, ha_bound⟩
    refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasFDerivWithinAt) fun x x_in ↦ ?_
    rw [← NNReal.coe_le_coe, coe_nnnorm, Real.coe_nnabs]
    exact (ha_bound x (hε x_in)).trans (le_abs_self _)
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : H → α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' x a) x
this_1 : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' x₀ a) x₀
this :
  ∀ᵐ (a : α) ∂μ,
    LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : H) ↦ F x a) (ball x₀ ε)
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀

Tactic:
apply (hasFDerivAt_integral_of_dominated_loc_of_lip (ball_mem_nhds x₀ ε_pos)
    hF_meas hF_int hF'_meas this bound_integrable diff_x₀).2

Premises used: Metric.ball_mem_nhds, And.right, hasFDerivAt_integral_of_dominated_loc_of_lip
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_4
inst_2 : NormedAddCommGroup H
x₀ : H
s : Set H
inst_3 : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ s, HasFDerivAt (fun (x : H) ↦ F x t) (F' x t) x
⊢ (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x

Tactic:
rw [ae_restrict_uIoc_iff] at h_diff h_bound

Premises used: MeasureTheory.ae_restrict_uIoc_iff
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_4
inst_2 : NormedAddCommGroup H
x₀ : H
s : Set H
inst_3 : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ s, HasFDerivAt (fun (x : H) ↦ F x t) (F' x t) x
h_bound₁ :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
⊢ IntervalIntegrable bound μ a b

Tactic:
rw [ae_restrict_uIoc_iff] at h_diff h_bound

Premises used: MeasureTheory.ae_restrict_uIoc_iff
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_4
inst_2 : NormedAddCommGroup H
x₀ : H
s : Set H
inst_3 : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ s, HasFDerivAt (fun (x : H) ↦ F x t) (F' x t) x
h_bound₁ :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable₁ : IntervalIntegrable bound μ a b
⊢ (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1

Tactic:
rw [ae_restrict_uIoc_iff] at h_diff h_bound

Premises used: MeasureTheory.ae_restrict_uIoc_iff
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_4
inst_2 : NormedAddCommGroup H
x₀ : H
s : Set H
inst_3 : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
⊢ AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc b a))

Tactic:
simp_rw [AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff, eventually_and] at hF_meas hF'_meas

Premises used: Filter.eventually_and, MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_4
inst_2 : NormedAddCommGroup H
x₀ : H
s : Set H
inst_3 : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
hF'_meas₁ :
  AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc b a))
⊢ (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧
    ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))

Tactic:
simp_rw [AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff, eventually_and] at hF_meas hF'_meas

Premises used: Filter.eventually_and, MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_4
inst_2 : NormedAddCommGroup H
x₀ : H
s : Set H
inst_3 : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_bound :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
hF'_meas :
  AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc b a))
hF_meas :
  (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧
    ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))
⊢ HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ)
    (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀

Tactic:
(hasFDerivAt_integral_of_dominated_of_fderiv_le hs hF_meas.1 hF_int.1 hF'_meas.1 h_bound.1
          bound_integrable.1 h_diff.1).sub
      (hasFDerivAt_integral_of_dominated_of_fderiv_le hs hF_meas.2 hF_int.2 hF'_meas.2 h_bound.2
        bound_integrable.2 h_diff.2)

Premises used: HasFDerivAt.sub, intervalIntegral, And.right, And.left, hasFDerivAt_integral_of_dominated_of_fderiv_le
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_4
inst_2 : NormedAddCommGroup H
x₀ : H
s : Set H
inst_3 : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_bound :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
hF'_meas :
  AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc b a))
hF_meas :
  (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧
    ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))
⊢ HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ)
    (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀

Tactic:
exact
    (hasFDerivAt_integral_of_dominated_of_fderiv_le hs hF_meas.1 hF_int.1 hF'_meas.1 h_bound.1
          bound_integrable.1 h_diff.1).sub
      (hasFDerivAt_integral_of_dominated_of_fderiv_le hs hF_meas.2 hF_int.2 hF'_meas.2 h_bound.2
        bound_integrable.2 h_diff.2)

Premises used: HasFDerivAt.sub, And.right, And.left, hasFDerivAt_integral_of_dominated_of_fderiv_le
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' a) x₀
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
⊢ ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀

Tactic:
replace h_diff : ∀ᵐ a ∂μ, HasFDerivAt (F · a) (L (F' a)) x₀ :=
    h_diff.mono fun x hx ↦ hx.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
⊢ AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ

Tactic:
have hm : AEStronglyMeasurable (L ∘ F') μ := L.continuous.comp_aestronglyMeasurable hF'_meas
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
⊢ Integrable (ε := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ

Tactic:
obtain ⟨hF'_int, key⟩ := hasFDerivAt_integral_of_dominated_loc_of_lip
    hs hF_meas hF_int hm h_lipsch bound_integrable h_diff

Premises used: hasFDerivAt_integral_of_dominated_loc_of_lip
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
hF'_int : Integrable (ε := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
⊢ HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (∫ (a : α), ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a ∂μ) x₀

Tactic:
obtain ⟨hF'_int, key⟩ := hasFDerivAt_integral_of_dominated_loc_of_lip
    hs hF_meas hF_int hm h_lipsch bound_integrable h_diff

Premises used: hasFDerivAt_integral_of_dominated_loc_of_lip
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
hF'_int : Integrable (ε := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
key :
  HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (∫ (a : α), ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a ∂μ) x₀
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ norm (E := 𝕜 →L[𝕜] E) (((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a)) μ

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

Premises used: MeasureTheory.integrable_norm_iff
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
hF'_int : Integrable (ε := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
key :
  HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (∫ (a : α), ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a ∂μ) x₀
hF'_int₁ : Integrable (ε := ℝ) (fun (a : α) ↦ norm (E := 𝕜 →L[𝕜] E) (((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a)) μ
⊢ HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (∫ (a : α), ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a ∂μ) x₀

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

Premises used: MeasureTheory.integrable_norm_iff
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
hF'_int : Integrable (ε := ℝ) (fun (a : α) ↦ norm (E := 𝕜 →L[𝕜] E) (((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a)) μ
key :
  HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (∫ (a : α), ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a ∂μ) x₀
⊢ Integrable F' μ

Tactic:
simpa [L, (· ∘ ·), integrable_norm_iff hF'_meas] using hF'_int

Premises used: Function.comp, MeasureTheory.integrable_norm_iff
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
hF'_int : Integrable (ε := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
key :
  HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (∫ (a : α), ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a ∂μ) x₀
⊢ Integrable F' μ

Tactic:
replace hF'_int : Integrable F' μ := by
    rw [← integrable_norm_iff hm] at hF'_int
    simpa [L, (· ∘ ·), integrable_norm_iff hF'_meas] using hF'_int
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
key :
  HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (∫ (a : α), ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
⊢ Integrable F' μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
⟨hF'_int, ?_⟩

Premises used: And.intro