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