Theorem: ResidueTheoremAtOrigin_aux1c (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₂ σ a b : ℝ
⊢ ContinuousOn (fun y => ↑y + I) [[a, b]]
Tactic:
fun_prop
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₂ σ a b : ℝ
⊢ ∀ x ∈ [[a, b]], ↑x + I ≠ 0
Tactic:
simp [Complex.ext_iff]
State after:
no goals