awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip :
  ∀ᵐ (t : ℝ) ∂μ,
    t ∈ Ι a b → LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound t)) (fun (x : H) ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x t) (F' t) x₀
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
bound_integrable₁ : IntervalIntegrable bound μ a b
⊢ IntervalIntegrable 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₀
have 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₀
Tactic: rw [← ae_restrict_iff' measurableSet_uIoc] at h_lip h_diff
Cleared hypotheses: h_lip, bound_integrable, h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (goal)
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_int : IntervalIntegrable (F x₀) μ 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
bound_integrable : IntervalIntegrable bound μ a b
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₀
⊢ IntervalIntegrable 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₀
have simp : ∀ (hF_int : IntegrableOn (F x₀) (Ι a b) μ) (bound_integrable : IntegrableOn bound (Ι a b) μ),
  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 [intervalIntegrable_iff] at hF_int bound_integrable ⊢
Cleared hypotheses: hF_int, bound_integrable
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (goal)
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) μ
⊢ 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₀
have 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₀
Tactic: simp only [intervalIntegral_eq_integral_uIoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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) μ
⊢ 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₀
have 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₀
Tactic: have := hasFDerivAt_integral_of_dominated_loc_of_lip hs hF_meas hF_int hF'_meas h_lip
    bound_integrable h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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
⊢ 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₀
have h_bound₁ : ∀ᵐ (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
Cleared hypotheses: h_bound, bound_integrable, h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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
⊢ 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₀
have 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
Tactic: rw [← ae_restrict_iff' measurableSet_uIoc] at h_bound h_diff
Cleared hypotheses: h_bound, bound_integrable, h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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
⊢ 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₀
have hF_int₁ : IntegrableOn (F x₀) (Ι a b) μ
Tactic: simp only [intervalIntegrable_iff] at hF_int bound_integrable
Cleared hypotheses: hF_int, bound_integrable
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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) μ
⊢ 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₀
have bound_integrable₁ : IntegrableOn bound (Ι a b) μ
Tactic: simp only [intervalIntegrable_iff] at hF_int bound_integrable
Cleared hypotheses: hF_int, bound_integrable
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (goal)
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.{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₀
have 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₀
Tactic: simp only [intervalIntegral_eq_integral_uIoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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₀
⊢ 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₀
have 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
Tactic: rw [← ae_restrict_iff' measurableSet_uIoc] at h_lipsch h_diff
Cleared hypotheses: h_lipsch, bound_integrable, h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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
⊢ 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₀
have h_diff₁ : ∀ᵐ (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
Cleared hypotheses: h_lipsch, bound_integrable, h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (goal)
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₀
⊢ 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₀
have 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₀
Tactic: simp only [intervalIntegrable_iff] at hF_int bound_integrable ⊢
Cleared hypotheses: hF_int, bound_integrable
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (goal)
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) μ
⊢ 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₀
have 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₀
Tactic: simp only [intervalIntegral_eq_integral_uIoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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) μ
⊢ 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₀
have 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₀
Tactic: have := hasDerivAt_integral_of_dominated_loc_of_lip hs hF_meas hF_int hF'_meas h_lipsch
    bound_integrable h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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
⊢ IntervalIntegrable (F' x₀) μ a b ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
have h_bound₁ : ∀ᵐ (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
Cleared hypotheses: h_bound, bound_integrable, h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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
h_bound₁ : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable₁ : IntervalIntegrable bound μ a b
⊢ IntervalIntegrable (F' x₀) μ a b ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
have h_diff₁ : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasDerivAt (fun (x_2 : 𝕜) ↦ F x_2 x) (F' x_1 x) x_1
Tactic: rw [← ae_restrict_iff' measurableSet_uIoc] at h_bound h_diff
Cleared hypotheses: h_bound, bound_integrable, h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (goal)
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 : ∀ᵐ (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, HasDerivAt (fun (x_2 : 𝕜) ↦ F x_2 x) (F' x_1 x) x_1
⊢ IntervalIntegrable (F' x₀) μ a b ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
have simp : ∀ (hF_int : IntegrableOn (F x₀) (Ι a b) μ) (bound_integrable : IntegrableOn bound (Ι a b) μ),
  IntegrableOn (F' x₀) (Ι a b) μ ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
Tactic: simp only [intervalIntegrable_iff] at hF_int bound_integrable ⊢
Cleared hypotheses: hF_int, bound_integrable
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (goal)
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'_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, HasDerivAt (fun (x_2 : 𝕜) ↦ F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
⊢ IntegrableOn (F' x₀) (Ι a b) μ ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
have simp : IntegrableOn (F' x₀) (Ι 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' x₀ t ∂μ)) x₀
Tactic: simp only [intervalIntegral_eq_integral_uIoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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'_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, HasDerivAt (fun (x_2 : 𝕜) ↦ F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
⊢ IntegrableOn (F' x₀) (Ι 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' x₀ t ∂μ)) x₀
have this : Integrable (F' x₀) (μ.restrict (Ι a b)) ∧
  HasDerivAt.{u_1, u_2} (F := E) (fun (n : 𝕜) ↦ ∫ (a : ℝ) in Ι a b, F n a ∂μ) (∫ (a : ℝ) in Ι a b, F' x₀ a ∂μ) x₀
Tactic: have := hasDerivAt_integral_of_dominated_loc_of_deriv_le hs hF_meas hF_int hF'_meas h_bound
    bound_integrable h_diff