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' μ
refine : HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
⊢ Integrable F' μ ∧
    HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
refine ⟨hF'_int, ?_⟩
-- 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' μ
pos :
  ∀ (hE : CompleteSpace E),
    HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
neg :
  ∀ (hE : ¬CompleteSpace E),
    HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- 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
neg :
  ∀ (hH : Subsingleton H),
    HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
neg₁ :
  ∀ (hH : Nontrivial H),
    HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
rcases subsingleton_or_nontrivial H with hH | hH

Premises used: subsingleton_or_nontrivial
-- 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
hH : Subsingleton H
⊢ Subsingleton (H →L[𝕜] E)

Tactic:
have : Subsingleton (H →L[𝕜] E) := inferInstance
-- 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
hH : Subsingleton H
this : Subsingleton (H →L[𝕜] E)
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) 0 x₀

Tactic:
hasFDerivAt_of_subsingleton _ x₀

Premises used: hasFDerivAt_of_subsingleton
-- 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
hH : Subsingleton H
this : Subsingleton (H →L[𝕜] E)
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
convert! hasFDerivAt_of_subsingleton _ x₀

Premises used: hasFDerivAt_of_subsingleton
-- 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
hH : Nontrivial H
⊢ ¬CompleteSpace (H →L[𝕜] E)

Tactic:
simpa [SeparatingDual.completeSpace_continuousLinearMap_iff] using hE

Premises used: SeparatingDual.completeSpace_continuousLinearMap_iff
-- 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
hH : Nontrivial H
⊢ ¬CompleteSpace (H →L[𝕜] E)

Tactic:
have : ¬(CompleteSpace (H →L[𝕜] E)) := by
        simpa [SeparatingDual.completeSpace_continuousLinearMap_iff] using hE
-- 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
hH : Nontrivial H
this : ¬CompleteSpace (H →L[𝕜] E)
neg : HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ 0) 0 x₀
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
simp only [integral, hE, ↓reduceDIte, this]

Premises used: reduceDIte, MeasureTheory.integral
-- 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
hH : Nontrivial H
this : ¬CompleteSpace (H →L[𝕜] E)
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ 0) 0 x₀

Tactic:
hasFDerivAt_const 0 x₀

Premises used: hasFDerivAt_const, OfNat.ofNat
-- 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
hH : Nontrivial H
this : ¬CompleteSpace (H →L[𝕜] E)
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ 0) 0 x₀

Tactic:
exact hasFDerivAt_const 0 x₀

Premises used: hasFDerivAt_const, OfNat.ofNat
-- 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
⊢ ball x₀ ε ∈ 𝓝 x₀

Tactic:
have h_ball : ball x₀ ε ∈ 𝓝 x₀ := ball_mem_nhds x₀ ε_pos
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →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₀
apply :
  ball x₀ ε ⊆
    {x : H |
      (fun (x : H) ↦
          ‖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}
⊢ ∀ᶠ (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:
apply mem_of_superset (ball_mem_nhds _ ε_pos)

Premises used: Metric.ball_mem_nhds, 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₀
x : H
x_in : x ∈ ball x₀ ε
hf : Integrable (F x) μ
hg : Integrable (F x₀) μ
hf₁ : Integrable.{u_3, u_1} (ε := E) (fun (a : α) ↦ F x a - F x₀ a) μ
hg₁ : Integrable.{u_3, u_1} (ε := E) (fun (a : α) ↦ (F' a : (a : H) → E) (x - x₀)) μ
⊢ Membership.mem (γ := Set H)
    {x : H |
      ‖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

Tactic:
rw [Set.mem_setOf_eq, ← norm_smul_of_nonneg (nneg _), integral_smul, integral_sub, integral_sub,
      ← ContinuousLinearMap.integral_apply hF'_int]

Premises used: ContinuousLinearMap.integral_apply, MeasureTheory.integral_smul, norm_smul_of_nonneg, MeasureTheory.integral_sub, Set.mem_setOf_eq
-- 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:
hF_int' x 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₀
x : H
x_in : x ∈ ball x₀ ε
⊢ Integrable (F x₀) μ

Tactic:
hF_int
-- 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.{u_3, u_1} (ε := E) (fun (a : α) ↦ F x a - F x₀ a) μ

Tactic:
(hF_int' x x_in).sub hF_int

Premises used: MeasureTheory.Integrable.sub
-- 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.{u_3, u_1} (ε := E) (fun (a : α) ↦ (F' a : (a : H) → E) (x - x₀)) μ

Tactic:
hF'_int.apply_continuousLinearMap _

Premises used: MeasureTheory.Integrable.apply_continuousLinearMap