awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
s : Finset ι
f : ι → ℂ → E
c : ℂ
R : ℝ
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), ∑ i ∈ s, f i z) (∑ i ∈ s, ∮ (z : ℂ) in C(c, R), f i z)

Tactic:
simp only [circleIntegral, Finset.smul_sum,
    intervalIntegral.integral_finsetSum fun i hi ↦ (h i hi).out]

Premises used: intervalIntegral.integral_finsetSum, Finset.smul_sum, circleIntegral, CircleIntegrable.out
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
⊢ ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ = |R| * ‖f (circleMap c R θ)‖

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
hbc : ‖f (circleMap c R θ)‖ ≤ C
⊢ |R| * ‖f (circleMap c R θ)‖ ≤ |R| * C

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
⊢ ‖f (circleMap c R θ)‖ ≤ C

Tactic:
hf _ <| circleMap_mem_sphere' _ _ _

Premises used: circleMap_mem_sphere'
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
⊢ ‖f (circleMap c R θ)‖ ≤ C

Tactic:
exact hf _ <| circleMap_mem_sphere' _ _ _

Premises used: circleMap_mem_sphere'
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
rw : |R| * C * (2 * π) = 2 * π * |R| * C
⊢ |R| * C * |2 * π - 0| = 2 * π * |R| * C

Tactic:
rw [sub_zero, _root_.abs_of_pos Real.two_pi_pos]

Premises used: sub_zero, Real.two_pi_pos, abs_of_pos
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
⊢ |R| * C * (2 * π) = 2 * π * |R| * C

Tactic:
ac_rfl
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : |R| = R
rwa rwa₁ rwa₂ rwa₃ : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C

Tactic:
rwa [this]
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : |R| = R
rw rw₁ : 2 * π * R * C = 2 * π * R * C
⊢ 2 * π * |R| * C = 2 * π * R * C

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖(2 * (↑π : ℂ) * I)⁻¹‖ = (2 * π)⁻¹

Tactic:
simp [Real.pi_pos.le]

Premises used: Real.pi_pos, LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖(2 * (↑π : ℂ) * I)⁻¹‖ = (2 * π)⁻¹

Tactic:
have : ‖(2 * π * I : ℂ)⁻¹‖ = (2 * π)⁻¹ := by simp [Real.pi_pos.le]
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * (↑π : ℂ) * I)⁻¹‖ = (2 * π)⁻¹
rw : norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) ≤ 2 * π * R * C
⊢ ‖HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), f z)‖ ≤ R * C

Tactic:
rw [norm_smul, this, ← div_eq_inv_mul, div_le_iff₀ Real.two_pi_pos, mul_comm (R * C), ← mul_assoc]

Premises used: div_le_iff₀, HMul.hMul, norm_smul, mul_assoc, Real.two_pi_pos, mul_comm, div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * (↑π : ℂ) * I)⁻¹‖ = (2 * π)⁻¹
⊢ norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) ≤ 2 * π * R * C

Tactic:
norm_integral_le_of_norm_le_const hR hf

Premises used: circleIntegral.norm_integral_le_of_norm_le_const
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * (↑π : ℂ) * I)⁻¹‖ = (2 * π)⁻¹
⊢ norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) ≤ 2 * π * R * C

Tactic:
exact norm_integral_le_of_norm_le_const hR hf

Premises used: circleIntegral.norm_integral_le_of_norm_le_const
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hlt : ∃ z ∈ sphere c R, ‖f z‖ < C
⊢ ∃ z ∈ circleMap c R '' Ioc 0 (2 * π), ‖f z‖ < C

Tactic:
rw [← _root_.abs_of_pos hR, ← image_circleMap_Ioc] at hlt

Premises used: image_circleMap_Ioc, abs_of_pos
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hlt : ∃ z ∈ circleMap c R '' Ioc 0 (2 * π), ‖f z‖ < C
rcases :
  ∀ (θ₀ : ℝ) (hmem : θ₀ ∈ Ioc 0 (2 * π)) (hlt : ‖f (circleMap c R θ₀)‖ < C),
    norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) < 2 * π * R * C
⊢ norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) < 2 * π * R * C

Tactic:
rcases hlt with ⟨_, ⟨θ₀, hmem, rfl⟩, hlt⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) ≤
    ∫ (θ : ℝ) in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖

Tactic:
intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le

Premises used: LT.lt.le, Real.two_pi_pos, intervalIntegral.norm_integral_le_integral_norm, circleIntegral
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
simp : LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, R * ‖f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)
⊢ LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)

Tactic:
simp only [deriv_circleMap, norm_smul, norm_mul, norm_circleMap_zero, abs_of_pos hR, norm_I,
        mul_one]

Premises used: norm_smul, norm_circleMap_zero, norm_mul, deriv_circleMap, Complex.norm_I, abs_of_pos, mul_one
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, R * ‖f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)

Tactic:
intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
          Real.two_pi_pos ?_ continuousOn_const (fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩

Premises used: intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt, Set.Ioc_subset_Icc_self, continuousOn_const, Real.two_pi_pos, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
refine_1 : ContinuousOn (Y := ℝ) (fun (θ : ℝ) ↦ R * ‖f (circleMap c R θ)‖) (Icc 0 (2 * π))
refine_2 : ∀ θ ∈ Ioc 0 (2 * π), R * ‖f (circleMap c R θ)‖ ≤ R * C
refine_3 : R * ‖f (circleMap c R θ₀)‖ < R * C
⊢ LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, R * ‖f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)

Tactic:
refine intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
          Real.two_pi_pos ?_ continuousOn_const (fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩

Premises used: intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt, Set.Ioc_subset_Icc_self, continuousOn_const, Real.two_pi_pos, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ContinuousOn (Y := ℝ) (fun (θ : ℝ) ↦ R * ‖f (circleMap c R θ)‖) (Icc 0 (2 * π))

Tactic:
continuousOn_const.mul (hc.comp (continuous_circleMap _ _).continuousOn fun θ _ =>
          circleMap_mem_sphere _ hR.le _).norm

Premises used: Continuous.continuousOn, continuousOn_const, LT.lt.le, continuous_circleMap, circleMap_mem_sphere, ContinuousOn.comp, ContinuousOn.norm, ContinuousOn.mul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ContinuousOn (Y := ℝ) (fun (θ : ℝ) ↦ R * ‖f (circleMap c R θ)‖) (Icc 0 (2 * π))

Tactic:
exact continuousOn_const.mul (hc.comp (continuous_circleMap _ _).continuousOn fun θ _ =>
          circleMap_mem_sphere _ hR.le _).norm

Premises used: Continuous.continuousOn, continuousOn_const, LT.lt.le, continuous_circleMap, circleMap_mem_sphere, ContinuousOn.comp, ContinuousOn.norm, ContinuousOn.mul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
θ : ℝ
h : θ ∈ Ioc 0 (2 * π)
refine_2 : ‖f (circleMap c R θ)‖ ≤ C
⊢ R * ‖f (circleMap c R θ)‖ ≤ R * C

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
θ : ℝ
h : θ ∈ Ioc 0 (2 * π)
⊢ ‖f (circleMap c R θ)‖ ≤ C

Tactic:
hf _ <| circleMap_mem_sphere _ hR.le _

Premises used: LT.lt.le, circleMap_mem_sphere
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
θ : ℝ
h : θ ∈ Ioc 0 (2 * π)
⊢ ‖f (circleMap c R θ)‖ ≤ C

Tactic:
exact hf _ <| circleMap_mem_sphere _ hR.le _

Premises used: LT.lt.le, circleMap_mem_sphere
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
refine_3 : 0 < R
⊢ R * ‖f (circleMap c R θ₀)‖ < R * C

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
simp : R * (2 * (π * C)) = 2 * (π * (R * C))
⊢ ∫ (x : ℝ) in 0..2 * π, R * C = 2 * π * R * C

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ R * (2 * (π * C)) = 2 * (π * (R * C))

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
z :
  LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)
z₁ : ∫ (x : ℝ) in 0..2 * π, R * C = 2 * π * R * C
⊢ norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) < 2 * π * R * C

Tactic:
calc
    ‖∮ z in C(c, R), f z‖ ≤ ∫ θ in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ :=
      intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le
    _ < ∫ _ in 0..2 * π, R * C := by
      simp only [deriv_circleMap, norm_smul, norm_mul, norm_circleMap_zero, abs_of_pos hR, norm_I,
        mul_one]
      refine intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
          Real.two_pi_pos ?_ continuousOn_const (fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩
      · exact continuousOn_const.mul (hc.comp (continuous_circleMap _ _).continuousOn fun θ _ =>
          circleMap_mem_sphere _ hR.le _).norm
      · gcongr
        exact hf _ <| circleMap_mem_sphere _ hR.le _
      · gcongr
    _ = 2 * π * R * C := by simp [mul_assoc]; ring

Premises used: LT.lt.le, Real.two_pi_pos, intervalIntegral.norm_integral_le_integral_norm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass 𝕜 ℂ E
a : 𝕜
f : ℂ → E
c : ℂ
R : ℝ
⊢ ∮ (z : ℂ) in C(c, R), a • f z = HSMul.hSMul (β := E) a (∮ (z : ℂ) in C(c, R), f z)

Tactic:
simp only [circleIntegral, ← smul_comm a (_ : ℂ) (_ : E), intervalIntegral.integral_smul]

Premises used: intervalIntegral.integral_smul, circleIntegral, SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → ℂ
a : E
c : ℂ
R : ℝ
⊢ ∮ (z : ℂ) in C(c, R), f z • a = HSMul.hSMul (α := ℂ) (∮ (z : ℂ) in C(c, R), f z) a

Tactic:
simp only [circleIntegral, intervalIntegral.integral_smul_const, ← smul_assoc]

Premises used: smul_assoc, intervalIntegral.integral_smul_const, circleIntegral
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
a : ℂ
f : ℂ → ℂ
c : ℂ
R : ℝ
⊢ ∮ (z : ℂ) in C(c, R), a * f z = a * ∮ (z : ℂ) in C(c, R), f z

Tactic:
integral_smul a f c R

Premises used: circleIntegral.integral_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
⊢ ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ = 2 * (↑π : ℂ) * I

Tactic:
simp [circleIntegral, ← div_eq_mul_inv, mul_div_cancel_left₀ _ (circleMap_ne_center hR)]

Premises used: mul_div_cancel_left₀, circleMap_ne_center, div_eq_mul_inv, circleIntegral
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
pos : ∀ (hi : CircleIntegrable f' c R), Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0
neg : ∀ (hi : ¬CircleIntegrable f' c R), Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0

Tactic:
by_cases hi : CircleIntegrable f' c R

Premises used: CircleIntegrable
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : 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
pos : ∮ (z : ℂ) in C(c, R), f' z = (f ∘ circleMap c R) (2 * π) - (f ∘ circleMap c R) 0
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0

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

Premises used: Iff.mpr, sub_eq_zero, periodic_circleMap, Function.Periodic.comp, Function.Periodic.eq
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : 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:
intervalIntegral.integral_eq_sub_of_hasDerivAt (fun θ _ => ?_) hi.out

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt, circleIntegral, CircleIntegrable.out
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : 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
pos :
  ∀ θ ∈ [[0, 2 * π]],
    HasDerivAt (f ∘ circleMap c R)
      (HSMul.hSMul (β := E) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ f' z) (circleMap 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

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt, CircleIntegrable.out
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : 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
θ : ℝ
h_1 : θ ∈ [[0, 2 * π]]
⊢ HasDerivAt (f ∘ circleMap c R)
    (HSMul.hSMul (β := E) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ f' z) (circleMap c R θ))) θ

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

Premises used: DifferentiableAt.hasDerivAt, HasDerivWithinAt.scomp_hasDerivAt, circleMap_mem_sphere', differentiable_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : 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
θ : ℝ
h_1 : θ ∈ [[0, 2 * π]]
⊢ HasDerivAt (f ∘ circleMap c R)
    (HSMul.hSMul (β := E) (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' _ _)

Premises used: DifferentiableAt.hasDerivAt, HasDerivWithinAt.scomp_hasDerivAt, circleMap_mem_sphere', differentiable_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : 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
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0

Tactic:
integral_undef hi

Premises used: circleIntegral.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : 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
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0

Tactic:
exact integral_undef hi

Premises used: circleIntegral.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
hR : 0 ≤ R
h : ∀ z ∈ sphere c R, HasDerivWithinAt f (f' z) (sphere c R) z
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0

Tactic:
integral_eq_zero_of_hasDerivWithinAt' <| (abs_of_nonneg hR).symm ▸ h

Premises used: circleIntegral.integral_eq_zero_of_hasDerivWithinAt'
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
inl : ∀ (hw : w ∈ sphere c |0|), Eq (α := ℂ) (∮ (z : ℂ) in C(c, 0), (z - w) ^ n) 0
inr : ∀ (h0 : R ≠ 0), Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0

Tactic:
rcases eq_or_ne R 0 with (rfl | h0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
c w : ℂ
hn : n < 0
hw : w ∈ sphere c |0|
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, 0), (z - w) ^ n) 0

Tactic:
apply integral_radius_zero

Premises used: circleIntegral.integral_radius_zero
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
h0 : R ≠ 0
inr : ¬CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0

Tactic:
apply integral_undef

Premises used: circleIntegral.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
h0 : R ≠ 0
⊢ ¬CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R

Tactic:
simpa [circleIntegrable_sub_zpow_iff, *, not_or] using mem_sphere_iff_norm.1 hw

Premises used: not_or, mem_sphere_iff_norm, circleIntegrable_sub_zpow_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
pos : ∀ (H : w ∈ sphere c |R| ∧ n < -1), Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
neg : ∀ (H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n), Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0

Tactic:
by_cases! H : w ∈ sphere c |R| ∧ n < -1

Premises used: abs, Metric.sphere
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| ∧ n < -1
⊢ w ∈ sphere c |R|

Tactic:
rcases H with ⟨hw, hn⟩
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| ∧ n < -1
hw : w ∈ sphere c |R|
⊢ n < -1

Tactic:
rcases H with ⟨hw, hn⟩
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn_1 : n ≠ -1
c w : ℂ
R : ℝ
hw : w ∈ sphere c |R|
hn : n < -1
⊢ LT.lt (α := ℤ) (-1) 0

Tactic:
decide
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn_1 : n ≠ -1
c w : ℂ
R : ℝ
hw : w ∈ sphere c |R|
hn : n < -1
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0

Tactic:
exact integral_sub_zpow_of_undef (hn.trans (by decide)) hw

Premises used: circleIntegral.integral_sub_zpow_of_undef, LT.lt.trans
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ HasDerivAt (fun (x : ℂ) ↦ ((fun (x : ℂ) ↦ x ^ (n + 1)) ∘ fun (x : ℂ) ↦ id x - w) x / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
    ((↑(n + 1) : ℂ) * (id z - w) ^ (n + 1 - 1) * 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) z

Tactic:
((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const
        _

Premises used: HasDerivAt.comp, HasDerivAt.sub_const, hasDerivAt_id, HAdd.hAdd, HasDerivAt.div_const, Or.imp, OfNat.ofNat, hasDerivAt_zpow