have h2 : Integrable (φ z₀) μ :=
  φ_cts.self_of_nhds.integrableOn_Icc.mono_set Ioc_subset_Icc_self
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a✝ b✝ t : ℝ
n : ℕ
φ : ℂ → ℝ → ℂ
ψ : ℝ → ℂ
z₀ : ℂ
a b C δ : ℝ
hab : a ≤ b
δ_pos : 0 < δ
φ_cts : ∀ᶠ (z : ℂ) in 𝓝 z₀, ContinuousOn (φ z) (Icc a b)
φ_der : ∀ t ∈ Ioc a b, HasDerivAt (fun x => φ x t) (ψ t) z₀
φ_lip : ∀ t ∈ Ioc a b, LipschitzOnWith (nnabs C) (fun x => φ x t) (ball z₀ δ)
ψ_cts : ContinuousOn ψ (Ioc a b)
μ : Measure ℝ := Measure.restrict volume (Ioc a b)
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AEStronglyMeasurable (φ z) μ
h2 : Integrable (φ z₀) μ
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioc a b, φ z x ∂volume) (∫ (x : ℝ) in Ioc a b, ψ x ∂volume) z₀