Theorem: Complex.inv_re_add_im (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₂ σ : ℝ
⊢ (↑x + ↑y * I)⁻¹ = (↑x - I * ↑y) / (↑x ^ 2 + ↑y ^ 2)
Tactic:
rw [Complex.inv_def, div_eq_mul_inv]
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₂ σ : ℝ
⊢ (starRingEnd ℂ) (↑x + ↑y * I) * ↑(normSq (↑x + ↑y * I))⁻¹ = (↑x - I * ↑y) * (↑x ^ 2 + ↑y ^ 2)⁻¹

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₂ σ : ℝ
⊢ (starRingEnd ℂ) (↑x + ↑y * I) * ↑(normSq (↑x + ↑y * I))⁻¹ = (↑x - I * ↑y) * (↑x ^ 2 + ↑y ^ 2)⁻¹
Tactic:
congr <;> simp [conj_ofReal, normSq] <;> ring
State after:
no goals