simp_rw [VerticalIntegral, VIntegral, ← smul_add]
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
⊢ VerticalIntegral f σ =
    (I • ∫ (t : ℝ) in Iic a, f (↑σ + ↑t * I)) + VIntegral f σ a b + I • ∫ (t : ℝ) in Ici b, f (↑σ + ↑t * I)
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
⊢ I • ∫ (t : ℝ), f (↑σ + ↑t * I) =
    I •
      (((∫ (t : ℝ) in Iic a, f (↑σ + ↑t * I)) + ∫ (t : ℝ) in a..b, f (↑σ + ↑t * I)) +
        ∫ (t : ℝ) in Ici b, f (↑σ + ↑t * I))