E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R : ℝ), Periodic (circleMap c R) (2 * π)
⊢ Periodic (circleTransformDeriv R z w f) (2 * π)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ Periodic (circleTransformDeriv R z w f) (2 * π)
have := periodic_circleMap
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
⊢ ∀ (x : ℝ), circleTransformDeriv R z w f (x + 2 * π) = circleTransformDeriv R z w f x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R : ℝ), Periodic (circleMap c R) (2 * π)
⊢ Periodic (circleTransformDeriv R z w f) (2 * π)
simp_rw [Periodic] at *
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ circleTransformDeriv R z w f (x + 2 * π) = circleTransformDeriv R z w f x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
⊢ ∀ (x : ℝ), circleTransformDeriv R z w f (x + 2 * π) = circleTransformDeriv R z w f x
intro x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ (2 * ↑π * I)⁻¹ • deriv (circleMap z R) (x + 2 * π) • ((circleMap z R x - w) ^ 2)⁻¹ • f (circleMap z R x) =
    (2 * ↑π * I)⁻¹ • deriv (circleMap z R) x • ((circleMap z R x - w) ^ 2)⁻¹ • f (circleMap z R x)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ circleTransformDeriv R z w f (x + 2 * π) = circleTransformDeriv R z w f x
simp_rw [circleTransformDeriv, this]
case e_a.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ deriv (circleMap z R) (x + 2 * π) = deriv (circleMap z R) x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ (2 * ↑π * I)⁻¹ • deriv (circleMap z R) (x + 2 * π) • ((circleMap z R x - w) ^ 2)⁻¹ • f (circleMap z R x) =
    (2 * ↑π * I)⁻¹ • deriv (circleMap z R) x • ((circleMap z R x - w) ^ 2)⁻¹ • f (circleMap z R x)
congr 2
no goals
case e_a.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ deriv (circleMap z R) (x + 2 * π) = deriv (circleMap z R) x
simp [this]