rw [Complex.inv_def, div_eq_mul_inv]
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)
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)⁻¹