rw [← intervalIntegral.integral_Iic_sub_Iic hf.restrict hf.restrict, add_sub_cancel,
  integral_Iic_eq_integral_Iio, intervalIntegral.integral_Iio_add_Ici hf.restrict hf.restrict]
case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ a b : ℝ
hf : Integrable (fun t => f (↑σ + ↑t * I)) volume
⊢ ∫ (t : ℝ), f (↑σ + ↑t * I) =
    ((∫ (t : ℝ) in Iic a, f (↑σ + ↑t * I)) + ∫ (t : ℝ) in a..b, f (↑σ + ↑t * I)) + ∫ (t : ℝ) in Ici b, f (↑σ + ↑t * I)
no goals