case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → HasDerivWithinAt f (f' z) (sphere c (Abs.abs R)) z
hi : CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = 0

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → HasDerivWithinAt f (f' z) (sphere c (Abs.abs R)) z
hi : ¬CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = 0
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → HasDerivWithinAt f (f' z) (sphere c (Abs.abs R)) z
⊢ (∮ (z : ℂ) in C(c, R), f' z) = 0
by_cases hi : CircleIntegrable f' c R
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → HasDerivWithinAt f (f' z) (sphere c (Abs.abs R)) z
hi : CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = (f ∘ circleMap c R) (2 * π) - (f ∘ circleMap c R) 0
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → HasDerivWithinAt f (f' z) (sphere c (Abs.abs R)) z
hi : CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = 0
rw [← sub_eq_zero.2 ((periodic_circleMap c R).comp f).eq]
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → HasDerivWithinAt f (f' z) (sphere c (Abs.abs R)) z
hi : CircleIntegrable f' c R
θ : ℝ
x✝ : θ ∈ [[0, 2 * π]]
⊢ HasDerivAt (f ∘ circleMap c R) (deriv (circleMap c R) θ • (fun z => f' z) (circleMap c R θ)) θ
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → HasDerivWithinAt f (f' z) (sphere c (Abs.abs R)) z
hi : CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = (f ∘ circleMap c R) (2 * π) - (f ∘ circleMap c R) 0
refine' intervalIntegral.integral_eq_sub_of_hasDerivAt (fun θ _ => _) hi.out
no goals
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → HasDerivWithinAt f (f' z) (sphere c (Abs.abs R)) z
hi : CircleIntegrable f' c R
θ : ℝ
x✝ : θ ∈ [[0, 2 * π]]
⊢ HasDerivAt (f ∘ circleMap c R) (deriv (circleMap c R) θ • (fun z => f' z) (circleMap c R θ)) θ
exact (h _ (circleMap_mem_sphere' _ _ _)).scomp_hasDerivAt θ
  (differentiable_circleMap _ _ _).hasDerivAt (circleMap_mem_sphere' _ _)
no goals
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ (z : ℂ), z ∈ sphere c (Abs.abs R) → HasDerivWithinAt f (f' z) (sphere c (Abs.abs R)) z
hi : ¬CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = 0
exact integral_undef hi