internlm/Lean-Github huggingface dataset:
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})
hleft : 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]]
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) = 0
h₈ : RectangleIntegral f (↑z₂.re + ↑z₁.im * I) (↑z₃.re + ↑z₂.im * I) = 0
hbot : RectangleBorderIntegrable f z₀ z₃
htop : RectangleBorderIntegrable f (↑z₀.re + ↑z₁.im * I) z₃
hright : RectangleBorderIntegrable f z₁ (↑z₃.re + ↑z₂.im * I)
hbot'' : Rectangle z₀ (↑z₃.re + ↑z₁.im * I) ⊆ Rectangle z₀ z₃ \ {p}
htop'' : Rectangle (↑z₀.re + ↑z₂.im * I) z₃ ⊆ Rectangle z₀ z₃ \ {p}
h₁ :
  RectangleIntegral f z₀ z₃ =
    RectangleIntegral f z₀ (↑z₃.re + ↑z₁.im * I) + RectangleIntegral f (↑z₀.re + ↑z₁.im * I) z₃
h₂ : RectangleIntegral f z₀ (↑z₃.re + ↑z₁.im * I) = 0
h₃ :
  RectangleIntegral f (↑z₀.re + ↑z₁.im * I) z₃ =
    RectangleIntegral f (↑z₀.re + ↑z₁.im * I) (↑z₃.re + ↑z₂.im * I) + RectangleIntegral f (↑z₀.re + ↑z₂.im * I) z₃
h₄ : RectangleIntegral f (↑z₀.re + ↑z₂.im * I) z₃ = 0
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₁ (↑z₃.re + ↑z₂.im * I)
h₇ :
  RectangleIntegral f z₁ (↑z₃.re + ↑z₂.im * I) =
    RectangleIntegral f z₁ z₂ + RectangleIntegral f (↑z₂.re + ↑z₁.im * I) (↑z₃.re + ↑z₂.im * I)
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Tactic:
additive_combination h₁ + h₂ + h₃ + h₄ + h₅ + h₆ + h₇ + h₈
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
⊢ p.re < z₂.re
Tactic:
linarith
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
⊢ p.re < z₃.re
Tactic:
linarith
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
⊢ p.im < z₂.im
Tactic:
linarith
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
⊢ p.im < z₃.im
Tactic:
linarith
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
⊢ z₀.re < p.re
Tactic:
linarith
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
⊢ z₁.re < p.re
Tactic:
linarith
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
⊢ z₀.im < p.im
Tactic:
linarith
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
⊢ z₁.im < p.im
Tactic:
linarith
Proof state after:
no goals
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_1.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})
⊢ z₀.re ≤ (↑z₀.re + ↑z₀.im * I).re ∧
    (↑z₀.re + ↑z₀.im * I).re ≤ (↑z₃.re + ↑z₃.im * I).re ∧
      (↑z₃.re + ↑z₃.im * I).re ≤ z₃.re ∧
        z₀.im ≤ (↑z₀.re + ↑z₀.im * I).im ∧
          (↑z₀.re + ↑z₀.im * I).im ≤ (↑z₃.re + ↑z₃.im * I).im ∧ (↑z₃.re + ↑z₃.im * I).im ≤ z₃.im
Tactic:
simp_all
Proof state after:
no goals
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_1.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})
⊢ p.re ≠ (↑z₀.re + ↑z₀.im * I).re ∧
    p.re ≠ (↑z₃.re + ↑z₃.im * I).re ∧ p.im ≠ (↑z₀.re + ↑z₀.im * I).im ∧ p.im ≠ (↑z₃.re + ↑z₃.im * I).im
Tactic:
simpa using ⟨by linarith, by linarith, by linarith, by linarith⟩
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole'
Proof 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
Proof state after:
no goals
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_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 }
Proof state after:
no goals
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_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
Proof state after:
no goals
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_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 }
Proof state after:
no goals
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_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
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole
Proof 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 w p : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, RectangleIntegral f z w = RectangleIntegral f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' zero_lt_one, SmallSquareInRectangle hp]
Proof state after:
case h
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 w p : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
⊢ ∀ a ∈ Ioo 0 1,
    Square p a ⊆ Rectangle z w → RectangleIntegral f z w = RectangleIntegral f (-↑a - I * ↑a + p) (↑a + I * ↑a + p)
Theorem: RectanglePullToNhdOfPole
Proof state before:
case h
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 w p : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
⊢ ∀ a ∈ Ioo 0 1,
    Square p a ⊆ Rectangle z w → RectangleIntegral f z w = RectangleIntegral f (-↑a - I * ↑a + p) (↑a + I * ↑a + p)
Tactic:
intro c ⟨cpos, _⟩ hc
Proof state after:
case h
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 w p : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
cpos : 0 < c
right✝ : c < 1
hc : Square p c ⊆ Rectangle z w
⊢ RectangleIntegral f z w = RectangleIntegral f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)