no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
this : Abs.abs R = R
⊢ ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → ‖f z‖ ≤ C
rwa [this]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
this : Abs.abs R = R
⊢ 2 * π * Abs.abs R * C = 2 * π * R * C
rw [this]