Theorem: RectanglePullToNhdOfPole'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.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₂ σ : ℝ
inst✝ : CompleteSpace E
z₀ z₁ z₂ z₃ p : ℂ
hp : Rectangle z₁ z₂ ∈ 𝓝 p
hz : Rectangle z₁ z₂ ⊆ Rectangle z₀ z₃
fHolo : HolomorphicOn f (Rectangle z₀ z₃ \ {p})
hz₀_re : z₀.re ≤ z₃.re
hz₀_im : z₀.im ≤ z₃.im
hz₁_re : z₁.re ≤ z₂.re
hz₁_im : z₁.im ≤ z₂.im
left✝¹¹ : z₀.re ≤ z₁.re
right✝⁷ : z₁.re ≤ z₃.re
left✝¹⁰ : z₀.im ≤ z₁.im
right✝⁶ : z₁.im ≤ z₃.im
left✝⁹ : z₀.re ≤ z₂.re
right✝⁵ : z₂.re ≤ z₃.re
left✝⁸ : z₀.im ≤ z₂.im
right✝⁴ : z₂.im ≤ z₃.im
left✝⁷ : z₁.re < p.re
right✝³ : p.re < z₂.re
left✝⁶ : z₁.im < p.im
right✝² : p.im < z₂.im
left✝⁵ : p.re < z₂.re
left✝⁴ : p.re < z₃.re
left✝³ : p.im < z₂.im
right✝¹ : p.im < z₃.im
left✝² : z₀.re < p.re
left✝¹ : z₁.re < p.re
left✝ : z₀.im < p.im
right✝ : z₁.im < p.im
fCont : ContinuousOn f (Rectangle z₀ z₃ \ {p})
hbot : RectangleBorderIntegrable f (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₃.im * I)
htop : RectangleBorderIntegrable f (↑z₀.re + ↑z₁.im * I) (↑z₃.re + ↑z₃.im * I)
hleft : RectangleBorderIntegrable f (↑z₀.re + ↑z₁.im * I) (↑z₃.re + ↑z₂.im * I)
hright : RectangleBorderIntegrable f (↑z₁.re + ↑z₁.im * I) (↑z₃.re + ↑z₂.im * I)
hbot' : z₁.im ∈ [[z₀.im, z₃.im]]
htop' : z₂.im ∈ [[z₁.im, z₃.im]]
hleft' : z₁.re ∈ [[z₀.re, z₃.re]]
hright' : z₂.re ∈ [[z₁.re, z₃.re]]
hbot'' : Rectangle (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₁.im * I) ⊆ Rectangle z₀ z₃ \ {p}
htop'' : Rectangle (↑z₀.re + ↑z₂.im * I) (↑z₃.re + ↑z₃.im * I) ⊆ Rectangle z₀ z₃ \ {p}
hleft'' : Rectangle (↑z₀.re + ↑z₁.im * I) (↑z₁.re + ↑z₂.im * I) ⊆ Rectangle z₀ z₃ \ {p}
hright'' : Rectangle (↑z₂.re + ↑z₁.im * I) (↑z₃.re + ↑z₂.im * I) ⊆ Rectangle z₀ z₃ \ {p}
h₁ :
  RectangleIntegral f (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₃.im * I) =
    RectangleIntegral f (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₁.im * I) +
      RectangleIntegral f (↑z₀.re + ↑z₁.im * I) (↑z₃.re + ↑z₃.im * I)
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Tactic:
have h₂ := fHolo.vanishesOnRectangle hbot''
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.refine_2.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₂ σ : ℝ
inst✝ : CompleteSpace E
z₀ z₁ z₂ z₃ p : ℂ
hp : Rectangle z₁ z₂ ∈ 𝓝 p
hz : Rectangle z₁ z₂ ⊆ Rectangle z₀ z₃
fHolo : HolomorphicOn f (Rectangle z₀ z₃ \ {p})
hz₀_re : z₀.re ≤ z₃.re
hz₀_im : z₀.im ≤ z₃.im
hz₁_re : z₁.re ≤ z₂.re
hz₁_im : z₁.im ≤ z₂.im
left✝¹¹ : z₀.re ≤ z₁.re
right✝⁷ : z₁.re ≤ z₃.re
left✝¹⁰ : z₀.im ≤ z₁.im
right✝⁶ : z₁.im ≤ z₃.im
left✝⁹ : z₀.re ≤ z₂.re
right✝⁵ : z₂.re ≤ z₃.re
left✝⁸ : z₀.im ≤ z₂.im
right✝⁴ : z₂.im ≤ z₃.im
left✝⁷ : z₁.re < p.re
right✝³ : p.re < z₂.re
left✝⁶ : z₁.im < p.im
right✝² : p.im < z₂.im
left✝⁵ : p.re < z₂.re
left✝⁴ : p.re < z₃.re
left✝³ : p.im < z₂.im
right✝¹ : p.im < z₃.im
left✝² : z₀.re < p.re
left✝¹ : z₁.re < p.re
left✝ : z₀.im < p.im
right✝ : z₁.im < p.im
fCont : ContinuousOn f (Rectangle z₀ z₃ \ {p})
hbot : RectangleBorderIntegrable f (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₃.im * I)
htop : RectangleBorderIntegrable f (↑z₀.re + ↑z₁.im * I) (↑z₃.re + ↑z₃.im * I)
hleft : RectangleBorderIntegrable f (↑z₀.re + ↑z₁.im * I) (↑z₃.re + ↑z₂.im * I)
hright : RectangleBorderIntegrable f (↑z₁.re + ↑z₁.im * I) (↑z₃.re + ↑z₂.im * I)
hbot' : z₁.im ∈ [[z₀.im, z₃.im]]
htop' : z₂.im ∈ [[z₁.im, z₃.im]]
hleft' : z₁.re ∈ [[z₀.re, z₃.re]]
hright' : z₂.re ∈ [[z₁.re, z₃.re]]
hbot'' : Rectangle (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₁.im * I) ⊆ Rectangle z₀ z₃ \ {p}
htop'' : Rectangle (↑z₀.re + ↑z₂.im * I) (↑z₃.re + ↑z₃.im * I) ⊆ Rectangle z₀ z₃ \ {p}
hleft'' : Rectangle (↑z₀.re + ↑z₁.im * I) (↑z₁.re + ↑z₂.im * I) ⊆ Rectangle z₀ z₃ \ {p}
hright'' : Rectangle (↑z₂.re + ↑z₁.im * I) (↑z₃.re + ↑z₂.im * I) ⊆ Rectangle z₀ z₃ \ {p}
h₁ :
  RectangleIntegral f (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₃.im * I) =
    RectangleIntegral f (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₁.im * I) +
      RectangleIntegral f (↑z₀.re + ↑z₁.im * I) (↑z₃.re + ↑z₃.im * I)
h₂ : RectangleIntegral f (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₁.im * I) = 0
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂