-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem integral_eq_zero_of_hasDerivWithinAt' [CompleteSpace E] {f f' : ℂ → E} {c : ℂ} {R : ℝ}
    (h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z) :
    (∮ z in C(c, R), f' z) = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
⊢ (∮ (z : ℂ) in C(c, R), f' z) = 0

Tactic:
by_cases hi : CircleIntegrable f' c R

Result:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |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 ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : ¬CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = 0

Proof state:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |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 θ)) θ

Tactic:
exact (h _ (circleMap_mem_sphere' _ _ _)).scomp_hasDerivAt θ
  (differentiable_circleMap _ _ _).hasDerivAt (circleMap_mem_sphere' _ _)

Result:
no goals

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

Tactic:
exact integral_undef hi

Result:
no goals

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

Tactic:
rw [← sub_eq_zero.2 ((periodic_circleMap c R).comp f).eq]

Result:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = (f ∘ circleMap c R) (2 * π) - (f ∘ circleMap c R) 0

Proof state:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : CircleIntegrable f' c R
⊢ (∮ (z : ℂ) in C(c, R), f' z) = (f ∘ circleMap c R) (2 * π) - (f ∘ circleMap c R) 0

Tactic:
refine intervalIntegral.integral_eq_sub_of_hasDerivAt (fun θ _ => ?_) hi.out

Result:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |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 θ)) θ