case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ circleTransformDeriv R z w f x✝ = (circleMap z R x✝ - w)⁻¹ • circleTransform R z w f x✝
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ circleTransformDeriv R z w f = fun θ => (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ
ext
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ ((2 * ↑π * I)⁻¹ * deriv (circleMap z R) x✝ * ((circleMap z R x✝ - w) ^ 2)⁻¹) • f (circleMap z R x✝) =
    ((circleMap z R x✝ - w)⁻¹ * (2 * ↑π * I)⁻¹ * deriv (circleMap z R) x✝ * (circleMap z R x✝ - w)⁻¹) •
      f (circleMap z R x✝)
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ circleTransformDeriv R z w f x✝ = (circleMap z R x✝ - w)⁻¹ • circleTransform R z w f x✝
simp_rw [circleTransformDeriv, circleTransform, ← mul_smul, ← mul_assoc]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (-(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2)⁻¹ *
        (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝) =
    ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (circleMap z R x✝ - w)⁻¹ ^ 2 * (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝)
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ ((2 * ↑π * I)⁻¹ * deriv (circleMap z R) x✝ * ((circleMap z R x✝ - w) ^ 2)⁻¹) • f (circleMap z R x✝) =
    ((circleMap z R x✝ - w)⁻¹ * (2 * ↑π * I)⁻¹ * deriv (circleMap z R) x✝ * (circleMap z R x✝ - w)⁻¹) •
      f (circleMap z R x✝)
ring_nf
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (-(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2)⁻¹ *
        (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝) =
    ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * ((circleMap z R x✝ - w) ^ 2)⁻¹ * (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝)
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (-(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2)⁻¹ *
        (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝) =
    ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (circleMap z R x✝ - w)⁻¹ ^ 2 * (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝)
rw [inv_pow]
case h.e_a.e_a.e_a.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ -(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2 = (circleMap z R x✝ - w) ^ 2
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (-(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2)⁻¹ *
        (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝) =
    ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * ((circleMap z R x✝ - w) ^ 2)⁻¹ * (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝)
congr
no goals
case h.e_a.e_a.e_a.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ -(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2 = (circleMap z R x✝ - w) ^ 2
ring