Theorem: verticalIntegral_split_three (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

State before:
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)
Tactic:
simp_rw [VerticalIntegral, VIntegral, ← smul_add]
State after:
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))

State before:
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))
Tactic:
congr
State after:
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)

State before:
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)
Tactic:
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]
State after:
no goals