Theorem: ResidueTheoremAtOrigin_aux2c (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 => 1 + ↑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]], 1 + ↑x * I ≠ 0
Tactic:
simp [Complex.ext_iff]
State after:
no goals