We could weaken FiniteDimensional ℝ H with SecondCountable (H →L[ℝ] E) if needed, but that is less convenient to work with.

theorem hasFDerivAt_parametric_primitive_of_lip' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [NormedAddCommGroup H] [NormedSpace ℝ H] (F : H → ℝ → E) (F' : ℝ → H →L[ℝ] E) {x₀ : H} {G' : H →L[ℝ] E} {bound : ℝ → ℝ} {s : H → ℝ} {ε : ℝ} (ε_pos : 0 < ε) {a a₀ b₀ : ℝ} {s' : H →L[ℝ] ℝ} (ha : a ∈ Set.Ioo a₀ b₀) (hsx₀ : s x₀ ∈ Set.Ioo a₀ b₀) (hF_meas : ∀ x ∈ Metric.ball x₀ ε, MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.volume.restrict (Set.Ioo a₀ b₀))) (hF_int : MeasureTheory.IntegrableOn (F x₀) (Set.Ioo a₀ b₀) MeasureTheory.volume) (hF_cont : ContinuousAt (F x₀) (s x₀)) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (MeasureTheory.volume.restrict (Ι a (s x₀)))) (h_lipsch : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a₀ b₀), LipschitzOnWith (Real.nnabs (bound t)) (fun (x : H) => F x t) (Metric.ball x₀ ε)) (bound_integrable : MeasureTheory.IntegrableOn bound (Set.Ioo a₀ b₀) MeasureTheory.volume) (bound_cont : ContinuousAt bound (s x₀)) (bound_nonneg : ∀ (t : ℝ), 0 ≤ bound t) (h_diff : ∀ᵐ (a : ℝ) ∂MeasureTheory.volume.restrict (Ι a (s x₀)), HasFDerivAt (fun (x : H) => F x a) (F' a) x₀) (s_diff : HasFDerivAt s s' x₀) (hG' : (∫ (t : ℝ) in a..s x₀, F' t) + (ContinuousLinearMap.toSpanSingleton ℝ (F x₀ (s x₀))).comp s' = G') : IntervalIntegrable F' MeasureTheory.volume a (s x₀) ∧ HasFDerivAt (fun (x : H) => ∫ (t : ℝ) in a..s x, F x t) G' x₀

This statement is a new version using the continuity note in mathlib. See commit 39e3f3f for an older version Maybe todo: let a depend on x.

theorem hasFDerivAt_parametric_primitive_of_contDiff' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] {F : H → ℝ → E} (hF : ContDiff ℝ 1 ↿F) {s : H → ℝ} (hs : ContDiff ℝ 1 s) (x₀ : H) (a : ℝ) : IntervalIntegrable (fun (t : ℝ) => fderiv ℝ (fun (x : H) => F x t) x₀) MeasureTheory.volume a (s x₀) ∧ HasFDerivAt (fun (x : H) => ∫ (t : ℝ) in a..s x, F x t) ((∫ (t : ℝ) in a..s x₀, fderiv ℝ (fun (x : H) => F x t) x₀) + (ContinuousLinearMap.toSpanSingleton ℝ (F x₀ (s x₀))).comp (fderiv ℝ s x₀)) x₀

theorem contDiff_parametric_primitive_of_contDiff' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] {F : H → ℝ → E} {n : ℕ} (hF : ContDiff ℝ ↑n ↿F) {s : H → ℝ} (hs : ContDiff ℝ (↑n) s) (a : ℝ) : ContDiff ℝ ↑n fun (x : H) => ∫ (t : ℝ) in a..s x, F x t

theorem contDiff_parametric_primitive_of_contDiff {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] {F : H → ℝ → E} {n : ℕ∞} (hF : ContDiff ℝ ↑n ↿F) {s : H → ℝ} (hs : ContDiff ℝ (↑n) s) (a : ℝ) : ContDiff ℝ ↑n fun (x : H) => ∫ (t : ℝ) in a..s x, F x t

theorem contDiff_parametric_primitive_of_contDiff'' {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] {F : H → ℝ → E} {n : ℕ∞} (hF : ContDiff ℝ ↑n ↿F) (a : ℝ) : ContDiff ℝ ↑n fun (x : H × ℝ) => ∫ (t : ℝ) in a..x.2, F x.1 t

theorem contDiff_parametric_integral_of_contDiff {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] {F : H → ℝ → E} {n : ℕ∞} (hF : ContDiff ℝ ↑n ↿F) (a b : ℝ) : ContDiff ℝ ↑n fun (x : H) => ∫ (t : ℝ) in a..b, F x t

theorem ContDiff.fderiv_parametric_integral {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] {F : H → ℝ → E} (hF : ContDiff ℝ 1 ↿F) (a b : ℝ) : (fderiv ℝ fun (x : H) => ∫ (t : ℝ) in a..b, F x t) = fun (x : H) => ∫ (t : ℝ) in a..b, fderiv ℝ (fun (x' : H) => F x' t) x