awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
h_diff :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
simp :
  IntegrableOn F' (Ι a b) μ ∧
    HasFDerivAt (fun (x : H) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
      (HSMul.hSMul (α := ℝ) (β := H →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' t ∂μ)) x₀
⊢ IntegrableOn F' (Ι a b) μ ∧
    HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ)
      (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
simp only [intervalIntegral_eq_integral_uIoc]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
h_diff :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
⊢ Integrable F' (μ.restrict (Ι a b)) ∧
    HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : ℝ) in Ι a b, F x a ∂μ)
      (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀

Tactic:
have := hasFDerivAt_integral_of_dominated_loc_of_lip hs hF_meas hF_int hF'_meas h_lip
    bound_integrable h_diff
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
h_diff :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
this :
  Integrable F' (μ.restrict (Ι a b)) ∧
    HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : ℝ) in Ι a b, F x a ∂μ)
      (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀
⊢ IntegrableOn F' (Ι a b) μ ∧
    HasFDerivAt (fun (x : H) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
      (HSMul.hSMul (α := ℝ) (β := H →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' t ∂μ)) x₀

Tactic:
⟨this.1, this.2.const_smul _⟩

Premises used: HasFDerivAt.const_smul, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
h_diff :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
this :
  Integrable F' (μ.restrict (Ι a b)) ∧
    HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : ℝ) in Ι a b, F x a ∂μ)
      (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀
⊢ IntegrableOn F' (Ι a b) μ ∧
    HasFDerivAt (fun (x : H) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
      (HSMul.hSMul (α := ℝ) (β := H →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' t ∂μ)) x₀

Tactic:
exact ⟨this.1, this.2.const_smul _⟩
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
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 : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x t) (F' x t) x
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_bound h_diff

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
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 : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x t) (F' x t) x
h_bound₁ : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
⊢ IntervalIntegrable bound μ a b

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_bound h_diff

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
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 : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x t) (F' x t) x
h_bound₁ : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable₁ : IntervalIntegrable bound μ a b
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    ∀ x_1 ∈ s, HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_bound h_diff

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
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 (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    ∀ x_1 ∈ s, HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
⊢ IntegrableOn (F x₀) (Ι a b) μ

Tactic:
simp only [intervalIntegrable_iff] at hF_int bound_integrable

Premises used: intervalIntegrable_iff
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
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 (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    ∀ x_1 ∈ s, HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
hF_int₁ : IntegrableOn (F x₀) (Ι a b) μ
⊢ IntegrableOn bound (Ι a b) μ

Tactic:
simp only [intervalIntegrable_iff] at hF_int bound_integrable

Premises used: intervalIntegrable_iff
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
h_diff :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    ∀ x_1 ∈ s, HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
simp :
  HasFDerivAt (fun (x : H) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
    (HSMul.hSMul (α := ℝ) (β := H →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ)) x₀
⊢ HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ)
    (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀

Tactic:
simp only [intervalIntegral_eq_integral_uIoc]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
h_diff :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    ∀ x_1 ∈ s, HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
⊢ HasFDerivAt (fun (x : H) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
    (HSMul.hSMul (α := ℝ) (β := H →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ)) x₀

Tactic:
(hasFDerivAt_integral_of_dominated_of_fderiv_le hs hF_meas hF_int hF'_meas h_bound
    bound_integrable h_diff).const_smul _

Premises used: HasFDerivAt.const_smul, hasFDerivAt_integral_of_dominated_of_fderiv_le
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
h_diff :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    ∀ x_1 ∈ s, HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
⊢ HasFDerivAt (fun (x : H) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
    (HSMul.hSMul (α := ℝ) (β := H →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ)) x₀

Tactic:
exact (hasFDerivAt_integral_of_dominated_of_fderiv_le hs hF_meas hF_int hF'_meas h_bound
    bound_integrable h_diff).const_smul _
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch :
  ∀ᵐ (t : ℝ) ∂μ,
    t ∈ Ι a b → LipschitzOnWith.{u_1, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound t)) (fun (x : 𝕜) ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasDerivAt (fun (x : 𝕜) ↦ F x t) (F' t) x₀
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_1, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : 𝕜) ↦ F x_1 x) s

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_lipsch h_diff

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch :
  ∀ᵐ (t : ℝ) ∂μ,
    t ∈ Ι a b → LipschitzOnWith.{u_1, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound t)) (fun (x : 𝕜) ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasDerivAt (fun (x : 𝕜) ↦ F x t) (F' t) x₀
h_lipsch₁ :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_1, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : 𝕜) ↦ F x_1 x) s
⊢ IntervalIntegrable bound μ a b

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_lipsch h_diff

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch :
  ∀ᵐ (t : ℝ) ∂μ,
    t ∈ Ι a b → LipschitzOnWith.{u_1, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound t)) (fun (x : 𝕜) ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasDerivAt (fun (x : 𝕜) ↦ F x t) (F' t) x₀
h_lipsch₁ :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_1, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : 𝕜) ↦ F x_1 x) s
bound_integrable₁ : IntervalIntegrable bound μ a b
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasDerivAt (fun (x_1 : 𝕜) ↦ F x_1 x) (F' x) x₀

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_lipsch h_diff

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_1, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : 𝕜) ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasDerivAt (fun (x_1 : 𝕜) ↦ F x_1 x) (F' x) x₀
simp :
  ∀ (hF_int : IntegrableOn (F x₀) (Ι a b) μ) (bound_integrable : IntegrableOn bound (Ι a b) μ),
    IntegrableOn F' (Ι a b) μ ∧
      HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
⊢ IntervalIntegrable F' μ a b ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
simp only [intervalIntegrable_iff] at hF_int bound_integrable ⊢

Premises used: intervalIntegrable_iff
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_1, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : 𝕜) ↦ F x_1 x) s
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasDerivAt (fun (x_1 : 𝕜) ↦ F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
simp :
  IntegrableOn F' (Ι a b) μ ∧
    HasDerivAt (fun (x : 𝕜) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
      (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' t ∂μ)) x₀
⊢ IntegrableOn F' (Ι a b) μ ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
simp only [intervalIntegral_eq_integral_uIoc]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_1, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : 𝕜) ↦ F x_1 x) s
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasDerivAt (fun (x_1 : 𝕜) ↦ F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
⊢ Integrable F' (μ.restrict (Ι a b)) ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (a : ℝ) in Ι a b, F x a ∂μ) (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀

Tactic:
have := hasDerivAt_integral_of_dominated_loc_of_lip hs hF_meas hF_int hF'_meas h_lipsch
    bound_integrable h_diff
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_1, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : 𝕜) ↦ F x_1 x) s
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasDerivAt (fun (x_1 : 𝕜) ↦ F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
this :
  Integrable F' (μ.restrict (Ι a b)) ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (a : ℝ) in Ι a b, F x a ∂μ) (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀
⊢ IntegrableOn F' (Ι a b) μ ∧
    HasDerivAt (fun (x : 𝕜) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
      (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' t ∂μ)) x₀

Tactic:
⟨this.1, this.2.const_smul _⟩

Premises used: HasDerivAt.const_smul, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_1, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : 𝕜) ↦ F x_1 x) s
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasDerivAt (fun (x_1 : 𝕜) ↦ F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
this :
  Integrable F' (μ.restrict (Ι a b)) ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (a : ℝ) in Ι a b, F x a ∂μ) (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀
⊢ IntegrableOn F' (Ι a b) μ ∧
    HasDerivAt (fun (x : 𝕜) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
      (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' t ∂μ)) x₀

Tactic:
exact ⟨this.1, this.2.const_smul _⟩
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) 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 : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x t) (F' x t) x
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_bound h_diff

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'