-- Mathlib/MeasureTheory/Integral/CircleTransform.lean
theorem circleTransformDeriv_periodic (f : ℂ → E) :
    Periodic (circleTransformDeriv R z w f) (2 * π)

Proof state:
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

Tactic:
intro x

Result:
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

Proof state:
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

Tactic:
simp [this]

Result:
no goals

Proof state:
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 * π)

Tactic:
simp_rw [Periodic] at *

Result:
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

Proof state:
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)

Tactic:
congr 2

Result:
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

Proof state:
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

Tactic:
simp_rw [circleTransformDeriv, this]

Result:
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)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ Periodic (circleTransformDeriv R z w f) (2 * π)

Tactic:
have := periodic_circleMap

Result:
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 * π)