all_goals refine intervalIntegral.integral_congr fun _ _ ↦ h ?_
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ HIntegral f z.re w.re z.im = HIntegral g z.re w.re z.im

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ HIntegral f z.re w.re w.im = HIntegral g z.re w.re w.im

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) = ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)

case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) = ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I)
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.re, w.re]]
⊢ ↑x✝¹ + ↑z.im * I ∈ RectangleBorder z w

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.re, w.re]]
⊢ ↑x✝¹ + ↑w.im * I ∈ RectangleBorder z w

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.im, w.im]]
⊢ ↑w.re + ↑x✝¹ * I ∈ RectangleBorder z w

case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[z.im, w.im]]
⊢ ↑z.re + ↑x✝¹ * I ∈ RectangleBorder z w