internlm/Lean-Github huggingface dataset:
Theorem: RectangleIntegralVSplit
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₂ σ b x₀ x₁ y₀ y₁ : ℝ
f_int_y₀_b_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume y₀ b
f_int_b_y₁_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume b y₁
f_int_y₀_b_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume y₀ b
f_int_b_y₁_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume b y₁
⊢ (((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
          ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
      I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I) =
    ((((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (b * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (b * 0 - 0 * 1), f (↑x + ↑(0 + (b * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (b * 1 + 0 * 0), f (↑(x₁ + (b * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (b * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀ + (b * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (b * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in x₀ + (b * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (b * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (b * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (b * 0 - 0 * 1)) + ↑y * I))
Tactic:
ring_nf
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ b x₀ x₁ y₀ y₁ : ℝ
f_int_y₀_b_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume y₀ b
f_int_b_y₁_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume b y₁
f_int_y₀_b_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume y₀ b
f_int_b_y₁_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume b y₁
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))
Theorem: RectangleIntegralVSplit
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₂ σ b x₀ x₁ y₀ y₁ : ℝ
f_int_y₀_b_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume y₀ b
f_int_b_y₁_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume b y₁
f_int_y₀_b_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume y₀ b
f_int_b_y₁_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume b y₁
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))
Tactic:
have h₁ := intervalIntegral.integral_add_adjacent_intervals f_int_y₀_b_left f_int_b_y₁_left
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ b x₀ x₁ y₀ y₁ : ℝ
f_int_y₀_b_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume y₀ b
f_int_b_y₁_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume b y₁
f_int_y₀_b_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume y₀ b
f_int_b_y₁_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume b y₁
h₁ :
  (∫ (x : ℝ) in y₀..b, f (↑x₀ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₀ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₀ + ↑x * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))
Theorem: RectangleIntegralVSplit
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₂ σ b x₀ x₁ y₀ y₁ : ℝ
f_int_y₀_b_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume y₀ b
f_int_b_y₁_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume b y₁
f_int_y₀_b_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume y₀ b
f_int_b_y₁_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume b y₁
h₁ :
  (∫ (x : ℝ) in y₀..b, f (↑x₀ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₀ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₀ + ↑x * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))
Tactic:
have h₂ := intervalIntegral.integral_add_adjacent_intervals f_int_y₀_b_right f_int_b_y₁_right
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ b x₀ x₁ y₀ y₁ : ℝ
f_int_y₀_b_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume y₀ b
f_int_b_y₁_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume b y₁
f_int_y₀_b_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume y₀ b
f_int_b_y₁_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume b y₁
h₁ :
  (∫ (x : ℝ) in y₀..b, f (↑x₀ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₀ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₀ + ↑x * I)
h₂ :
  (∫ (x : ℝ) in y₀..b, f (↑x₁ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₁ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₁ + ↑x * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))
Theorem: RectangleIntegralVSplit
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₂ σ b x₀ x₁ y₀ y₁ : ℝ
f_int_y₀_b_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume y₀ b
f_int_b_y₁_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume b y₁
f_int_y₀_b_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume y₀ b
f_int_b_y₁_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume b y₁
h₁ :
  (∫ (x : ℝ) in y₀..b, f (↑x₀ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₀ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₀ + ↑x * I)
h₂ :
  (∫ (x : ℝ) in y₀..b, f (↑x₁ + ↑x * I)) + ∫ (x : ℝ) in b..y₁, f (↑x₁ + ↑x * I) = ∫ (x : ℝ) in y₀..y₁, f (↑x₁ + ↑x * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) +
          I • ∫ (y : ℝ) in y₀..b, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..b, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑b * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in b..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in b..y₁, f (↑x₀ + ↑y * I))
Tactic:
additive_combination I • h₁ - I • h₂
Proof state after:
no goals
Theorem: RectangleIntegralVSplit'
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₂ σ b x₀ x₁ y₀ y₁ : ℝ
hb : b ∈ [[y₀, y₁]]
hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * I) (↑x₁ + ↑y₁ * I)
⊢ IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume y₀ y₁
Tactic:
simpa using hf.2.2.2
Proof state after:
no goals
Theorem: RectangleIntegralVSplit'
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₂ σ b x₀ x₁ y₀ y₁ : ℝ
hb : b ∈ [[y₀, y₁]]
hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * I) (↑x₁ + ↑y₁ * I)
⊢ IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume y₀ y₁
Tactic:
simpa using hf.2.2.1
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 : ℂ
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₂
Tactic:
obtain ⟨hz₀_re, hz₀_im, hz₁_re, hz₁_im⟩ := h_orientation
Proof state after:
case intro.intro.intro
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
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Theorem: RectanglePullToNhdOfPole'
Proof state before:
case intro.intro.intro
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
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Tactic:
have := rect_subset_iff.mp hz
Proof state after:
case intro.intro.intro
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
this : z₁ ∈ Rectangle z₀ z₃ ∧ z₂ ∈ Rectangle z₀ z₃
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Theorem: RectanglePullToNhdOfPole'
Proof state before:
case intro.intro.intro
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
this : z₁ ∈ Rectangle z₀ z₃ ∧ z₂ ∈ Rectangle z₀ z₃
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Tactic:
rw [Rectangle, uIcc_of_le hz₀_re, uIcc_of_le hz₀_im] at this
Proof state after:
case intro.intro.intro
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
this : z₁ ∈ Icc z₀.re z₃.re ×ℂ Icc z₀.im z₃.im ∧ z₂ ∈ Icc z₀.re z₃.re ×ℂ Icc z₀.im z₃.im
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Theorem: RectanglePullToNhdOfPole'
Proof state before:
case intro.intro.intro
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
this : z₁ ∈ Icc z₀.re z₃.re ×ℂ Icc z₀.im z₃.im ∧ z₂ ∈ Icc z₀.re z₃.re ×ℂ Icc z₀.im z₃.im
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Tactic:
obtain ⟨⟨⟨_, _⟩, ⟨_, _⟩⟩, ⟨_, _⟩, ⟨_, _⟩⟩ := this
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Theorem: RectanglePullToNhdOfPole'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Tactic:
obtain ⟨⟨_, _⟩, ⟨_, _⟩⟩ := (uIoo_of_le hz₁_re) ▸ (uIoo_of_le hz₁_im) ▸ rectangle_mem_nhds_iff.mp hp
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Theorem: RectanglePullToNhdOfPole'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Tactic:
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⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Theorem: RectanglePullToNhdOfPole'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Tactic:
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⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
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
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
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂
Tactic:
have fCont := fHolo.continuousOn
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
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})
⊢ RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂