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