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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
x : H
x_in : x ∈ ball x₀ ε
⊢ Integrable (F x) μ

Tactic:
exacts [hF_int' x x_in, hF_int, (hF_int' x x_in).sub hF_int,
      hF'_int.apply_continuousLinearMap _]

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.Integrable.apply_continuousLinearMap
-- 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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
⊢ ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)

Tactic:
have : ∀ᶠ x in 𝓝 x₀, ‖x - x₀‖⁻¹ * ‖((∫ a, F x a ∂μ) - ∫ a, F x₀ a ∂μ) - (∫ a, F' a ∂μ) (x - x₀)‖ =
      ‖∫ a, ‖x - x₀‖⁻¹ • (F x a - F x₀ a - F' a (x - x₀)) ∂μ‖ := by
    apply mem_of_superset (ball_mem_nhds _ ε_pos)
    intro x x_in; simp only
    rw [Set.mem_setOf_eq, ← norm_smul_of_nonneg (nneg _), integral_smul, integral_sub, integral_sub,
      ← ContinuousLinearMap.integral_apply hF'_int]
    exacts [hF_int' x x_in, hF_int, (hF_int' x x_in).sub hF_int,
      hF'_int.apply_continuousLinearMap _]
-- 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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (a : α), ‖x₀ - x₀‖⁻¹ • HSub.hSub (β := E) (F x₀ a - F x₀ a) ((F' a : (a : H) → E) (x₀ - x₀) : E) ∂μ) 0

Tactic:
simp
-- 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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
pos :
  Tendsto.{u_4, u_3} (β := E)
    (fun (x : H) ↦ ∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
    (𝓝 x₀) (𝓝 (∫ (a : α), ‖x₀ - x₀‖⁻¹ • HSub.hSub (β := E) (F x₀ a - F x₀ a) ((F' a : (a : H) → E) (x₀ - x₀) : E) ∂μ))
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
rw [hasFDerivAt_iff_tendsto, tendsto_congr' this, ← tendsto_zero_iff_norm_tendsto_zero, ←
    show (∫ a : α, ‖x₀ - x₀‖⁻¹ • (F x₀ a - F x₀ a - (F' a) (x₀ - x₀)) ∂μ) = 0 by simp]

Premises used: hasFDerivAt_iff_tendsto, tendsto_zero_iff_norm_tendsto_zero, Filter.tendsto_congr'
-- 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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
pos :
  ∀ᶠ (n : H) in 𝓝 x₀,
    AEStronglyMeasurable.{u_1, u_3} (β := E)
      (fun (a : α) ↦ ‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)) μ
pos₁ :
  ∀ᶠ (n : H) in 𝓝 x₀,
    ∀ᵐ (a : α) ∂μ, ‖‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)‖ ≤ b a + ‖F' a‖
pos₂ : Integrable (ε := ℝ) (fun (a : α) ↦ b a + ‖F' a‖) μ
pos₃ :
  ∀ᵐ (a : α) ∂μ,
    Tendsto (fun (n : H) ↦ ‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)) (𝓝 x₀)
      (𝓝 (‖x₀ - x₀‖⁻¹ • HSub.hSub (β := E) (F x₀ a - F x₀ a) ((F' a : (a : H) → E) (x₀ - x₀) : E)))
pos₄ : α → ℝ
⊢ Tendsto.{u_4, u_3} (β := E)
    (fun (x : H) ↦ ∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
    (𝓝 x₀) (𝓝 (∫ (a : α), ‖x₀ - x₀‖⁻¹ • HSub.hSub (β := E) (F x₀ a - F x₀ a) ((F' a : (a : H) → E) (x₀ - x₀) : E) ∂μ))

Tactic:
apply tendsto_integral_filter_of_dominated_convergence

Premises used: MeasureTheory.tendsto_integral_filter_of_dominated_convergence
-- 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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
h :
  ∀ (a : H) (x_in : a ∈ ball x₀ ε),
    AEStronglyMeasurable.{u_1, u_3} (β := E)
      (fun (a_1 : α) ↦ ‖a - x₀‖⁻¹ • HSub.hSub (β := E) (F a a_1 - F x₀ a_1) ((F' a_1 : (a : H) → E) (a - x₀) : E)) μ
⊢ ∀ᶠ (n : H) in 𝓝 x₀,
    AEStronglyMeasurable.{u_1, u_3} (β := E)
      (fun (a : α) ↦ ‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)) μ

Tactic:
filter_upwards [h_ball] with _ 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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
a : H
x_in : a ∈ ball x₀ ε
h :
  AEStronglyMeasurable.{u_1, u_3} (β := E)
    (fun (a_1 : α) ↦ HSub.hSub (β := E) (F a a_1 - F x₀ a_1) ((F' a_1 : (a : H) → E) (a - x₀) : E)) μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := E)
    (fun (a_1 : α) ↦ ‖a - x₀‖⁻¹ • HSub.hSub (β := E) (F a a_1 - F x₀ a_1) ((F' a_1 : (a : H) → E) (a - x₀) : E)) μ

Tactic:
apply AEStronglyMeasurable.const_smul

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul
-- 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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
a : H
x_in : a ∈ ball x₀ ε
⊢ AEStronglyMeasurable.{u_1, u_3} (β := E)
    (fun (a_1 : α) ↦ HSub.hSub (β := E) (F a a_1 - F x₀ a_1) ((F' a_1 : (a : H) → E) (a - x₀) : E)) μ

Tactic:
((hF_meas _ (hε x_in)).sub (hF_meas _ (hε x₀_in))).sub
      (hF'_meas.apply_continuousLinearMap _)

Premises used: MeasureTheory.AEStronglyMeasurable.sub, MeasureTheory.AEStronglyMeasurable.apply_continuousLinearMap
-- 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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
a : H
x_in : a ∈ ball x₀ ε
⊢ AEStronglyMeasurable.{u_1, u_3} (β := E)
    (fun (a_1 : α) ↦ HSub.hSub (β := E) (F a a_1 - F x₀ a_1) ((F' a_1 : (a : H) → E) (a - x₀) : E)) μ

Tactic:
exact ((hF_meas _ (hε x_in)).sub (hF_meas _ (hε x₀_in))).sub
      (hF'_meas.apply_continuousLinearMap _)

Premises used: MeasureTheory.AEStronglyMeasurable.sub, MeasureTheory.AEStronglyMeasurable.apply_continuousLinearMap
-- 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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
⊢ ∀ᶠ (n : H) in 𝓝 x₀,
    ∀ᵐ (a : α) ∂μ, ‖‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)‖ ≤ b a + ‖F' a‖

Tactic:
mem_of_superset h_ball fun x hx ↦ ?_

Premises used: Filter.Eventually, Filter.mem_of_superset
-- 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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
pos :
  ∀ (x : H) (hx : x ∈ ball x₀ ε),
    Membership.mem (γ := Set H)
      {x : H |
        (fun (n : H) ↦
            ∀ᵐ (a : α) ∂μ,
              ‖‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)‖ ≤ b a + ‖F' a‖)
          x}
      x
⊢ ∀ᶠ (n : H) in 𝓝 x₀,
    ∀ᵐ (a : α) ∂μ, ‖‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)‖ ≤ b a + ‖F' a‖

Tactic:
refine mem_of_superset h_ball fun x hx ↦ ?_

Premises used: Filter.mem_of_superset
-- 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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
x : H
hx : x ∈ ball x₀ ε
pos :
  ∀ (x_1 : α),
    (HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x x_1) (F' x_1) x₀ ∧
        ∀ x ∈ ball x₀ ε, ‖F x x_1 - F x₀ x_1‖ ≤ b x_1 * ‖x - x₀‖) →
      ‖‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x x_1 - F x₀ x_1) ((F' x_1 : (a : H) → E) (x - x₀) : E)‖ ≤ b x_1 + ‖F' x_1‖
pos₁ : α → ℝ
⊢ Membership.mem (γ := Set H)
    {x : H |
      (fun (n : H) ↦
          ∀ᵐ (a : α) ∂μ,
            ‖‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)‖ ≤ b a + ‖F' a‖)
        x}
    x

Tactic:
apply (h_diff.and h_lipsch).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 →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
x : H
hx : x ∈ ball x₀ ε
pos :
  ∀ (a : α) (ha_bound : ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖),
    ‖‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E)‖ ≤ b a + ‖F' a‖
⊢ ∀ (x_1 : α),
    (HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x x_1) (F' x_1) x₀ ∧
        ∀ x ∈ ball x₀ ε, ‖F x x_1 - F x₀ x_1‖ ≤ b x_1 * ‖x - x₀‖) →
      ‖‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x x_1 - F x₀ x_1) ((F' x_1 : (a : H) → E) (x - x₀) : E)‖ ≤ b x_1 + ‖F' x_1‖

Tactic:
on_goal 1 => rintro a ⟨-, ha_bound⟩