no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → ‖f z‖ ≤ C
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ = Abs.abs R * ‖f (circleMap c R θ)‖
simp [norm_smul]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → ‖f z‖ ≤ C
⊢ Abs.abs R * C * (2 * π) = 2 * π * Abs.abs R * C
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → ‖f z‖ ≤ C
⊢ Abs.abs R * C * Abs.abs (2 * π - 0) = 2 * π * Abs.abs R * C
rw [sub_zero, _root_.abs_of_pos Real.two_pi_pos]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → ‖f z‖ ≤ C
⊢ Abs.abs R * C * (2 * π) = 2 * π * Abs.abs R * C
ac_rfl