linarith
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
⊢ p.im < z₃.im
no goals