awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_lip :
  ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound t)) (fun (x : H) ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun (x : H) ↦ F x t) (F' t) x₀
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.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))
h_lip₁ :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
⊢ IntervalIntegrable bound μ a b

Tactic:
rw [ae_restrict_uIoc_iff] at h_lip h_diff

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 →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_lip :
  ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound t)) (fun (x : H) ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun (x : H) ↦ F x t) (F' t) x₀
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.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))
h_lip₁ :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
bound_integrable₁ : IntervalIntegrable bound μ a b
⊢ (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀

Tactic:
rw [ae_restrict_uIoc_iff] at h_lip h_diff

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 →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_lip :
  ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound t)) (fun (x : H) ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun (x : H) ↦ F x t) (F' t) x₀
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.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))
h_lip₁ :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
bound_integrable₁ : IntervalIntegrable bound μ a b
h_diff₁ :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀
⊢ AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.restrict (Set.Ioc b a))

Tactic:
rw [ae_restrict_uIoc_iff] at h_lip h_diff

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 →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_lip :
  ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound t)) (fun (x : H) ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun (x : H) ↦ F x t) (F' t) x₀
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.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))
h_lip₁ :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
bound_integrable₁ : IntervalIntegrable bound μ a b
h_diff₁ :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀
hF'_meas₁ : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.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:
rw [ae_restrict_uIoc_iff] at h_lip h_diff

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 →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_lip :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.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))
⊢ Integrable F' (μ.restrict (Set.Ioc a b)) ∧
    HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (a : ℝ) in Set.Ioc a b, F x a ∂μ)
      (∫ (a : ℝ) in Set.Ioc a b, F' a ∂μ) x₀

Tactic:
have H₁ :=
    hasFDerivAt_integral_of_dominated_loc_of_lip hs hF_meas.1 hF_int.1 hF'_meas.1 h_lip.1
      bound_integrable.1 h_diff.1
-- 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 →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_lip :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.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))
H₁ :
  Integrable F' (μ.restrict (Set.Ioc a b)) ∧
    HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (a : ℝ) in Set.Ioc a b, F x a ∂μ)
      (∫ (a : ℝ) in Set.Ioc a b, F' a ∂μ) x₀
⊢ Integrable F' (μ.restrict (Set.Ioc b a)) ∧
    HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (a : ℝ) in Set.Ioc b a, F x a ∂μ)
      (∫ (a : ℝ) in Set.Ioc b a, F' a ∂μ) x₀

Tactic:
have H₂ :=
    hasFDerivAt_integral_of_dominated_loc_of_lip hs hF_meas.2 hF_int.2 hF'_meas.2 h_lip.2
      bound_integrable.2 h_diff.2
-- 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 →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_lip :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.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))
H₁ :
  Integrable F' (μ.restrict (Set.Ioc a b)) ∧
    HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (a : ℝ) in Set.Ioc a b, F x a ∂μ)
      (∫ (a : ℝ) in Set.Ioc a b, F' a ∂μ) x₀
H₂ :
  Integrable F' (μ.restrict (Set.Ioc b a)) ∧
    HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (a : ℝ) in Set.Ioc b a, F x a ∂μ)
      (∫ (a : ℝ) in Set.Ioc b a, F' a ∂μ) x₀
⊢ IntervalIntegrable F' μ a b ∧
    HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ)
      x₀

Tactic:
⟨⟨H₁.1, H₂.1⟩, H₁.2.sub H₂.2⟩

Premises used: HasFDerivAt.sub, And.right, And.left, And.intro
-- 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 →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_lip :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a),
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.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))
H₁ :
  Integrable F' (μ.restrict (Set.Ioc a b)) ∧
    HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (a : ℝ) in Set.Ioc a b, F x a ∂μ)
      (∫ (a : ℝ) in Set.Ioc a b, F' a ∂μ) x₀
H₂ :
  Integrable F' (μ.restrict (Set.Ioc b a)) ∧
    HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (a : ℝ) in Set.Ioc b a, F x a ∂μ)
      (∫ (a : ℝ) in Set.Ioc b a, F' a ∂μ) x₀
⊢ IntervalIntegrable F' μ a b ∧
    HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ)
      x₀

Tactic:
exact ⟨⟨H₁.1, H₂.1⟩, H₁.2.sub H₂.2⟩
-- 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
rcases :
  ∀ (ε : ℝ) (ε_pos : ε > 0) (hε : ball x₀ ε ⊆ s),
    HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀

Tactic:
rcases Metric.mem_nhds_iff.1 hs with ⟨ε, ε_pos, hε⟩

Premises used: Metric.mem_nhds_iff, Iff.mp
-- 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₀ ∈ ball x₀ ε

Tactic:
have x₀_in : x₀ ∈ ball x₀ ε := mem_ball_self ε_pos
-- 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₀ ε
⊢ ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' x₀ a) x₀

Tactic:
have diff_x₀ : ∀ᵐ a ∂μ, HasFDerivAt (F · a) (F' x₀ a) x₀ :=
    h_diff.mono fun a ha ↦ ha x₀ (hε x₀_in)
-- 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₀
apply :
  ∀ (x : α),
    ((∀ x_1 ∈ s, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1) ∧
        ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) →
      LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x)
        (ball x₀ ε)
⊢ ∀ᵐ (a : α) ∂μ,
    LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : H) ↦ F x a) (ball x₀ ε)

Tactic:
apply (h_diff.and h_bound).mono

Premises used: Filter.Eventually.and, Filter.Eventually.mono
-- 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 : α
ha_deriv : ∀ x ∈ s, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
⊢ LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : H) ↦ F x a) (ball x₀ ε)

Tactic:
(convex_ball _ _).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasFDerivWithinAt) fun x x_in ↦ ?_

Premises used: HasFDerivAt.hasFDerivWithinAt, Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le, convex_ball
-- 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 : α
ha_deriv : ∀ x ∈ s, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
refine : ∀ (x : H) (x_in : x ∈ ball x₀ ε), ‖F' x a‖₊ ≤ (Real.nnabs : (a : ℝ) → NNReal) (bound a)
⊢ LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : H) ↦ F x a) (ball x₀ ε)

Tactic:
refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasFDerivWithinAt) fun x x_in ↦ ?_

Premises used: HasFDerivAt.hasFDerivWithinAt, Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le, convex_ball
-- 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 : α
ha_deriv : ∀ x ∈ s, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : H
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖ ≤ |bound a|

Tactic:
(ha_bound x (hε x_in)).trans (le_abs_self _)

Premises used: le_abs_self, LE.le.trans
-- 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 : α
ha_deriv : ∀ x ∈ s, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : H
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖ ≤ |bound a|

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

Premises used: le_abs_self, LE.le.trans