Theorem: ResidueTheoremAtOrigin (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₂ σ : ℝ
⊢ RectangleIntegral' (fun s => 1 / s) (-1 - I) (1 + I) = 1
Tactic:
rw [RectangleIntegral', ResidueTheoremAtOrigin']
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ (1 / (2 * ↑π * I)) • (2 * I * ↑π * 1) = 1

case h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ (-1 - I).re < 0

case h2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ (-1 - I).im < 0

case h3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ 0 < (1 + I).re

case h4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ 0 < (1 + I).im

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₂ σ : ℝ
⊢ (1 / (2 * ↑π * I)) • (2 * I * ↑π * 1) = 1

case h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ (-1 - I).re < 0

case h2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ (-1 - I).im < 0

case h3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ 0 < (1 + I).re

case h4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ 0 < (1 + I).im
Tactic:
all_goals { field_simp [pi_ne_zero] <;> ring }
State after:
no goals

State before:
case h4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ 0 < (1 + I).im
Tactic:
field_simp [pi_ne_zero] <;> ring
State after:
no goals