-- Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean
theorem hasFDerivAt_integral_of_dominated_loc_of_lip
    {F : H → ℝ → E} {F' : ℝ → H →L[𝕜] E} {x₀ : H}
    (ε_pos : 0 < ε) (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_lip : ∀ᵐ t ∂μ, t ∈ Ι a b →
      LipschitzOnWith (Real.nnabs <| bound t) (fun x => F x t) (ball x₀ ε))
    (bound_integrable : IntervalIntegrable bound μ a b)
    (h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → HasFDerivAt (fun x => F x t) (F' t) x₀) :
    IntervalIntegrable F' μ a b ∧
      HasFDerivAt (fun x => ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' t ∂μ) x₀

Proof state:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
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 (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (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 ⊢

Result:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
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 (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (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) μ ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Proof state:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
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 (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (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) μ ∧
    HasFDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀

Tactic:
have := hasFDerivAt_integral_of_dominated_loc_of_lip ε_pos hF_meas hF_int hF'_meas h_lip
  bound_integrable h_diff

Result:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
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 (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (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)) ∧
    HasFDerivAt (fun x => ∫ (a : ℝ) in Ι a b, F x a ∂μ) (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀
⊢ IntegrableOn F' (Ι a b) μ ∧
    HasFDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀

Proof state:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
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 (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (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) μ ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
simp only [intervalIntegral_eq_integral_uIoc]

Result:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
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 (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (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) μ ∧
    HasFDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀

Proof state:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
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 (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (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)) ∧
    HasFDerivAt (fun x => ∫ (a : ℝ) in Ι a b, F x a ∂μ) (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀
⊢ IntegrableOn F' (Ι a b) μ ∧
    HasFDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀

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

Result:
no goals