awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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 : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lip :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : H) ↦ F x a) s
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δ_meas : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ
hδε : ∀ x ∈ ball x₀ δ, x ∈ s
⊢ Integrable F' μ ∧
    HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have h_lip₁ : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖
Tactic: replace h_lip : ∀ᵐ a : α ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖ :=
    h_lip.mono fun a lip x hx ↦ lip.norm_sub_le (hδε x hx) (mem_of_mem_nhds hs)
Cleared hypotheses: h_lip
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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 : H) in 𝓝 x₀, 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δ_meas : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ
hδε : ∀ x ∈ ball x₀ δ, x ∈ s
h_lip : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖
⊢ Integrable F' μ ∧
    HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have bound_integrable₁ : Integrable (ε := ℝ) (fun (a : α) ↦ ‖bound a‖) μ
Tactic: replace bound_integrable := bound_integrable.norm
Cleared hypotheses: bound_integrable
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (goal)
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 : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
δ : ℝ
δ_pos : δ > 0
hδ_meas : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ
hδε : ∀ x ∈ ball x₀ δ, x ∈ s
h_lip : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖
bound_integrable : Integrable (ε := ℝ) (fun (a : α) ↦ ‖bound a‖) μ
hF_meas₁ : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ
hF_int₁ : Integrable (F x₀) μ
hF'_meas₁ : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖
⊢ Integrable F' μ ∧
    HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have bound_integrable₁ : Integrable (ε := ℝ) (fun (a : α) ↦ |bound a|) μ
Tactic: apply hasFDerivAt_integral_of_dominated_loc_of_lip' (ball_mem_nhds x₀ δ_pos)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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_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 : ℝ) ∂μ.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₀
⊢ 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₀
have hF'_meas₁ : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.restrict (Set.Ioc b a))
Tactic: simp_rw [AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff, eventually_and] at hF_meas hF'_meas
Cleared hypotheses: hF_meas, hF'_meas
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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_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 : ℝ) ∂μ.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))
⊢ 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₀
have 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))
Tactic: simp_rw [AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff, eventually_and] at hF_meas hF'_meas
Cleared hypotheses: hF_meas, hF'_meas
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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))
⊢ 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₀
have 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
Tactic: rw [ae_restrict_uIoc_iff] at h_lip h_diff
Cleared hypotheses: h_lip, bound_integrable, h_diff, hF'_meas, hF_meas
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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
⊢ 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₀
have 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₀
Tactic: rw [ae_restrict_uIoc_iff] at h_lip h_diff
Cleared hypotheses: h_lip, bound_integrable, h_diff, hF'_meas, hF_meas
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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))
⊢ 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₀
have 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₀
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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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₀
⊢ 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₀
have 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₀
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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (goal)
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
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
have 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₀
Tactic: rcases Metric.mem_nhds_iff.1 hs with ⟨ε, ε_pos, hε⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
have x₀_in : x₀ ∈ ball x₀ ε
Tactic: have x₀_in : x₀ ∈ ball x₀ ε := mem_ball_self ε_pos
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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₀ ε
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
have diff_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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : H → α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' x a) x
this : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' x₀ a) x₀
⊢ ∀ᵐ (a : α) ∂μ,
    LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : H) ↦ F x a) (ball x₀ ε)
have 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₀ ε)
Tactic: apply (h_diff.and h_bound).mono
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (goal)
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₀ ε)
have refine : ∀ (x : H) (x_in : x ∈ ball x₀ ε), ‖F' x a‖₊ ≤ (Real.nnabs : (a : ℝ) → NNReal) (bound a)
Tactic: refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasFDerivWithinAt) fun x x_in ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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₀
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
have this₁ : ∀ᵐ (a : α) ∂μ,
  LipschitzOnWith.{u_4, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : H) ↦ F x a) (ball x₀ ε)
Tactic: have : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (F · a) (ball x₀ ε) := by
    apply (h_diff.and h_bound).mono
    rintro a ⟨ha_deriv, ha_bound⟩
    refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasFDerivWithinAt) fun x x_in ↦ ?_
    rw [← NNReal.coe_le_coe, coe_nnnorm, Real.coe_nnabs]
    exact (ha_bound x (hε x_in)).trans (le_abs_self _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_4
inst_2 : NormedAddCommGroup H
x₀ : H
s : Set H
inst_3 : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ s, HasFDerivAt (fun (x : H) ↦ F x t) (F' x t) x
⊢ HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ)
    (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
have h_bound₁ : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
  ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
Tactic: rw [ae_restrict_uIoc_iff] at h_diff h_bound
Cleared hypotheses: h_bound, bound_integrable, h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_4
inst_2 : NormedAddCommGroup H
x₀ : H
s : Set H
inst_3 : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ s, HasFDerivAt (fun (x : H) ↦ F x t) (F' x t) x
h_bound₁ :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable₁ : IntervalIntegrable bound μ a b
⊢ HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ)
    (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
have h_diff₁ : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1) ∧
  ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
Tactic: rw [ae_restrict_uIoc_iff] at h_diff h_bound
Cleared hypotheses: h_bound, bound_integrable, h_diff