RectanglePullToNhdOfPole'

lemma RectanglePullToNhdOfPole' [CompleteSpace E] {z₀ z₁ z₂ z₃ p : ℂ}    (h_orientation : z₀.re ≤ z₃.re ∧ z₀.im ≤ z₃.im ∧      z₁.re ≤ z₂.re ∧ z₁.im ≤ z₂.im)    (hp : Rectangle z₁ z₂ ∈ 𝓝 p) (hz : Rectangle z₁ z₂ ⊆ Rectangle z₀ z₃)    (fHolo : HolomorphicOn f (Rectangle z₀ z₃ \ {p})) :    RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂ := by  obtain ⟨hz₀_re, hz₀_im, hz₁_re, hz₁_im⟩ := h_orientation  have := rect_subset_iff.mp hz  rw [Rectangle, uIcc_of_le hz₀_re, uIcc_of_le hz₀_im] at this  obtain ⟨⟨⟨_, _⟩, ⟨_, _⟩⟩, ⟨_, _⟩, ⟨_, _⟩⟩ := this  obtain ⟨⟨_, _⟩, ⟨_, _⟩⟩ :=    (uIoo_of_le hz₁_re) ▸ (uIoo_of_le hz₁_im) ▸ rectangle_mem_nhds_iff.mp hp  obtain ⟨_, _, _, _⟩ := show      p.re < z₂.re ∧ p.re < z₃.re ∧ p.im < z₂.im ∧ p.im < z₃.im from    ⟨by linarith, by linarith, by linarith, by linarith⟩  obtain ⟨_, _, _, _⟩ := show      z₀.re < p.re ∧ z₁.re < p.re ∧ z₀.im < p.im ∧ z₁.im < p.im from    ⟨by linarith, by linarith, by linarith, by linarith⟩  have fCont := fHolo.continuousOn  have hbot : RectangleBorderIntegrable f (↑z₀.re + ↑z₀.im * I)      (↑z₃.re + ↑z₃.im * I) := ?_  have htop : RectangleBorderIntegrable f (↑z₀.re + ↑z₁.im * I)      (↑z₃.re + ↑z₃.im * I) := ?_  have hleft : RectangleBorderIntegrable f (↑z₀.re + ↑z₁.im * I)      (↑z₃.re + ↑z₂.im * I) := ?_  have hright : RectangleBorderIntegrable f (↑z₁.re + ↑z₁.im * I)      (↑z₃.re + ↑z₂.im * I) := ?_  all_goals try {    refine ContinuousOn.rectangleBorder_integrable      (fCont.mono (rectangleBorder_subset_punctured_rect ?_ ?_))    · simp_all    · simpa using ⟨by linarith, by linarith, by linarith, by linarith⟩  }  have hbot' : z₁.im ∈ [[z₀.im, z₃.im]] := ?_  have htop' : z₂.im ∈ [[z₁.im, z₃.im]] := ?_  have hleft' : z₁.re ∈ [[z₀.re, z₃.re]] := ?_  have hright' : z₂.re ∈ [[z₁.re, z₃.re]] := ?_  all_goals try {    rw [Set.uIcc_of_le]    constructor    all_goals assumption  }  have hbot'' : Rectangle (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₁.im * I) ⊆    Rectangle z₀ z₃ \ {p} := ?_  have htop'' : Rectangle (↑z₀.re + ↑z₂.im * I) (↑z₃.re + ↑z₃.im * I) ⊆    Rectangle z₀ z₃ \ {p} := ?_  have hleft'' : Rectangle (↑z₀.re + ↑z₁.im * I) (↑z₁.re + ↑z₂.im * I) ⊆    Rectangle z₀ z₃ \ {p} := ?_  have hright'' : Rectangle (↑z₂.re + ↑z₁.im * I) (↑z₃.re + ↑z₂.im * I) ⊆    Rectangle z₀ z₃ \ {p} := ?_  all_goals try { apply rectangle_subset_punctured_rect <;> simp_all }  have h₁ := RectangleIntegralVSplit' hbot' hbot  have h₂ := fHolo.vanishesOnRectangle hbot''  have h₃ := RectangleIntegralVSplit' htop' htop  have h₄ := fHolo.vanishesOnRectangle htop''  have h₅ := RectangleIntegralHSplit' hleft' hleft  have h₆ := fHolo.vanishesOnRectangle hleft''  have h₇ := RectangleIntegralHSplit' hright' hright  have h₈ := fHolo.vanishesOnRectangle hright''  simp only [re_add_im] at *  additive_combination h₁ + h₂ + h₃ + h₄ + h₅ + h₆ + h₇ + h₈