Theorem: RectanglePullToNhdOfPole' (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₂ σ : ℝ
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})
⊢ ¬p.re = z₀.re
Tactic:
linarith
State after:
no goals

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₂ σ : ℝ
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})
⊢ ¬p.re = z₃.re
Tactic:
linarith
State after:
no goals

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₂ σ : ℝ
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})
⊢ ¬p.im = z₀.im
Tactic:
linarith
State after:
no goals

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₂ σ : ℝ
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})
⊢ ¬p.im = z₃.im
Tactic:
linarith
State after:
no goals

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_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₂ σ : ℝ
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)
⊢ z₁.im ∈ [[z₀.im, z₃.im]]
Tactic:
try { rw [Set.uIcc_of_le]; constructor; all_goals assumption }
State after:
no goals

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_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₂ σ : ℝ
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)
⊢ z₁.im ∈ [[z₀.im, z₃.im]]
Tactic:
rw [Set.uIcc_of_le]
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_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₂ σ : ℝ
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)
⊢ z₁.im ∈ Icc z₀.im z₃.im

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_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₂ σ : ℝ
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)
⊢ z₀.im ≤ z₃.im

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_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₂ σ : ℝ
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)
⊢ z₁.im ∈ Icc z₀.im z₃.im

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_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₂ σ : ℝ
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)
⊢ z₀.im ≤ z₃.im
Tactic:
constructor
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_1.left
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)
⊢ z₀.im ≤ z₁.im

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_1.right
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)
⊢ z₁.im ≤ z₃.im

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_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₂ σ : ℝ
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)
⊢ z₀.im ≤ z₃.im

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_1.left
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)
⊢ z₀.im ≤ z₁.im

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_1.right
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)
⊢ z₁.im ≤ z₃.im

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_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₂ σ : ℝ
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)
⊢ z₀.im ≤ z₃.im
Tactic:
all_goals assumption
State after:
no goals

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_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₂ σ : ℝ
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)
⊢ z₀.im ≤ z₃.im
Tactic:
assumption
State after:
no goals

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_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₂ σ : ℝ
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]]
⊢ Rectangle (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₁.im * I) ⊆ Rectangle z₀ z₃ \ {p}
Tactic:
try { apply rectangle_subset_punctured_rect <;> simp_all }
State after:
no goals

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_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₂ σ : ℝ
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]]
⊢ Rectangle (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₁.im * I) ⊆ Rectangle z₀ z₃ \ {p}
Tactic:
apply rectangle_subset_punctured_rect <;> simp_all
State after:
no goals