Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0,
    VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
have : Icc σ σ' ×ℂ univ ∈ 𝓝 p := by
  rw [← mem_interior_iff_mem_nhds, Complex.interior_reProdIm, interior_Icc, interior_univ]
  refine ⟨⟨?_, ?_⟩, trivial⟩ <;> linarith
State after:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0,
    VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)

State before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0,
    VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
obtain ⟨c', hc'0, hc'⟩ := ((nhds_hasBasis_square p).1 _).mp this
State after:
case intro.intro
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0,
    VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)

State before:
case intro.intro
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0,
    VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' hc'0] with c ⟨hc0, hcc'⟩
State after:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
⊢ VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)

State before:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
⊢ VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
have hsub : Square p c ⊆ Icc σ σ' ×ℂ univ := (square_subset_square hc0 hcc'.le).trans hc'
State after:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
⊢ VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)

State before:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
⊢ VerticalIntegral f σ' - VerticalIntegral f σ = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
apply tendsto_nhds_unique (RectangleIntegral_tendsTo_VerticalIntegral hbot htop hleft hright)
State after:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
⊢ Tendsto (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T)) atTop
    (𝓝 (RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)))

State before:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
⊢ Tendsto (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T)) atTop
    (𝓝 (RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)))
Tactic:
apply Filter.EventuallyEq.tendsto
State after:
case h.hf
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
⊢ (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T)) =ᶠ[atTop] fun x =>
    RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)

State before:
case h.hf
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
⊢ (fun T => RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T)) =ᶠ[atTop] fun x =>
    RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
filter_upwards [Filter.Ioi_mem_atTop ((c - p.im) ⊔ (c + p.im))] with y hy
State after:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)

State before:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
have : c - p.im < y ∧ c + p.im < y := sup_lt_iff.mp hy
State after:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝ : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this : c - p.im < y ∧ c + p.im < y
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)

State before:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝ : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this : c - p.im < y ∧ c + p.im < y
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
have : c + σ ≤ p.re := by simpa using (hsub ⟨left_mem_uIcc, left_mem_uIcc⟩).1.1
State after:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝¹ : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝ : c - p.im < y ∧ c + p.im < y
this : c + σ ≤ p.re
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)

State before:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝¹ : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝ : c - p.im < y ∧ c + p.im < y
this : c + σ ≤ p.re
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
have : c + p.re ≤ σ' := by simpa using (hsub ⟨right_mem_uIcc, right_mem_uIcc⟩).1.2
State after:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)

State before:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
apply RectanglePullToNhdOfPole'
State after:
case h.h_orientation
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ (↑σ - I * ↑y).re ≤ (↑σ' + I * ↑y).re ∧
    (↑σ - I * ↑y).im ≤ (↑σ' + I * ↑y).im ∧
      (-↑c - ↑c * I + p).re ≤ (↑c + ↑c * I + p).re ∧ (-↑c - ↑c * I + p).im ≤ (↑c + ↑c * I + p).im

case h.hp
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (-↑c - ↑c * I + p) (↑c + ↑c * I + p) ∈ 𝓝 ?h.p

case h.hz
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (-↑c - ↑c * I + p) (↑c + ↑c * I + p) ⊆ Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y)

case h.fHolo
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ HolomorphicOn f (Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y) \ {?h.p})

case h.p
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ ℂ

State before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Icc σ σ' ×ℂ univ ∈ 𝓝 p
Tactic:
rw [← mem_interior_iff_mem_nhds, Complex.interior_reProdIm, interior_Icc, interior_univ]
State after:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ p ∈ Ioo σ σ' ×ℂ univ

State before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ p ∈ Ioo σ σ' ×ℂ univ
Tactic:
refine ⟨⟨?_, ?_⟩, trivial⟩ <;> linarith
State after:
no goals

State before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝ : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this : c - p.im < y ∧ c + p.im < y
⊢ c + σ ≤ p.re
Tactic:
simpa using (hsub ⟨left_mem_uIcc, left_mem_uIcc⟩).1.1
State after:
no goals

State before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝¹ : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝ : c - p.im < y ∧ c + p.im < y
this : c + σ ≤ p.re
⊢ c + p.re ≤ σ'
Tactic:
simpa using (hsub ⟨right_mem_uIcc, right_mem_uIcc⟩).1.2
State after:
no goals

State before:
case h.h_orientation
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ (↑σ - I * ↑y).re ≤ (↑σ' + I * ↑y).re ∧
    (↑σ - I * ↑y).im ≤ (↑σ' + I * ↑y).im ∧
      (-↑c - ↑c * I + p).re ≤ (↑c + ↑c * I + p).re ∧ (-↑c - ↑c * I + p).im ≤ (↑c + ↑c * I + p).im
Tactic:
simpa using ⟨by linarith, by linarith, by linarith⟩
State after:
no goals

State before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ σ ≤ σ'
Tactic:
linarith
State after:
no goals

State before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ 0 ≤ y
Tactic:
linarith
State after:
no goals

State before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ 0 ≤ c
Tactic:
linarith
State after:
no goals

State before:
case h.hp
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (-↑c - ↑c * I + p) (↑c + ↑c * I + p) ∈ 𝓝 ?h.p
Tactic:
exact square_mem_nhds p (ne_of_gt hc0)
State after:
no goals

State before:
case h.hz
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (-↑c - ↑c * I + p) (↑c + ↑c * I + p) ⊆ Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y)
Tactic:
apply RectSubRect' <;> simpa using by linarith
State after:
no goals

State before:
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ c + p.im ≤ y
Tactic:
linarith
State after:
no goals

State before:
case h.fHolo
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ HolomorphicOn f (Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y) \ {p})
Tactic:
refine hf.mono (diff_subset_diff ?_ subset_rfl)
State after:
case h.fHolo
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y) ⊆ Icc σ σ' ×ℂ univ

State before:
case h.fHolo
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y) ⊆ Icc σ σ' ×ℂ univ
Tactic:
simpa [Rectangle, uIcc_of_lt (hσ.1.trans hσ.2)] using fun x ⟨hx, _⟩ ↦ ⟨hx, trivial⟩
State after:
no goals