awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
n : ℕ
refine_1 :
  AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ circleMap 0 R x * I)
    (Measure.restrict volume (Ι 0 (2 * π)))
refine_1₁ :
  AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ (w / (circleMap c R x - c)) ^ n)
    (Measure.restrict volume (Ι 0 (2 * π)))
refine_1₂ :
  AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ (circleMap c R x - c)⁻¹)
    (Measure.restrict volume (Ι 0 (2 * π)))
⊢ AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace)
    (fun (θ : ℝ) ↦
      (circleMap 0 R θ * I) • (w / (circleMap c R θ - c)) ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ))
    (Measure.restrict volume (Ι 0 (2 * π)))

Tactic:
apply_rules [AEStronglyMeasurable.smul, hf.def'.1]

Premises used: And.left, IntervalIntegrable.def', MeasureTheory.AEStronglyMeasurable.smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
n : ℕ
refine_1 : Measurable (β := ℂ) fun (x : ℝ) ↦ circleMap 0 R x * I
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ circleMap 0 R x * I)
    (Measure.restrict volume (Ι 0 (2 * π)))

Tactic:
apply Measurable.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
n : ℕ
refine_1 : Measurable (β := ℂ) fun (x : ℝ) ↦ (w / (circleMap c R x - c)) ^ n
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ (w / (circleMap c R x - c)) ^ n)
    (Measure.restrict volume (Ι 0 (2 * π)))

Tactic:
apply Measurable.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
n : ℕ
refine_1 : Measurable (β := ℂ) fun (x : ℝ) ↦ (circleMap c R x - c)⁻¹
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ (circleMap c R x - c)⁻¹)
    (Measure.restrict volume (Ι 0 (2 * π)))

Tactic:
apply Measurable.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
n : ℕ
⊢ Measurable (β := ℂ) fun (x : ℝ) ↦ circleMap 0 R x * I

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
n : ℕ
⊢ Measurable (β := ℂ) fun (x : ℝ) ↦ (w / (circleMap c R x - c)) ^ n

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
n : ℕ
⊢ Measurable (β := ℂ) fun (x : ℝ) ↦ (circleMap c R x - c)⁻¹

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
n : ℕ
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      ‖HSMul.hSMul (β := E) (deriv (circleMap c R) t)
            ((fun (z : ℂ) ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))‖ ≤
        (fun (n : ℕ) (θ : ℝ) ↦ ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) n t

Tactic:
simp [norm_smul, abs_of_pos hR, mul_left_comm R, inv_mul_cancel_left₀ hR.ne', mul_comm ‖_‖]

Premises used: Norm.norm, norm_smul, inv_mul_cancel_left₀, mul_left_comm, LT.lt.ne', mul_comm, abs_of_pos
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) → Summable (α := ℝ) fun (n : ℕ) ↦ (fun (n : ℕ) (θ : ℝ) ↦ ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) n t

Tactic:
Eventually.of_forall fun _ _ => (summable_geometric_of_lt_one hwR.1 hwR.2).mul_left _

Premises used: Norm.norm, circleMap, Filter.Eventually.of_forall, Summable.mul_left, And.right, And.left, summable_geometric_of_lt_one
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) → Summable (α := ℝ) fun (n : ℕ) ↦ (fun (n : ℕ) (θ : ℝ) ↦ ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) n t

Tactic:
exact Eventually.of_forall fun _ _ => (summable_geometric_of_lt_one hwR.1 hwR.2).mul_left _

Premises used: Filter.Eventually.of_forall, Summable.mul_left, And.right, And.left, summable_geometric_of_lt_one
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
⊢ IntervalIntegrable (ε := ℝ)
    (fun (t : ℝ) ↦ ∑' (n : ℕ), (fun (n : ℕ) (θ : ℝ) ↦ ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) n t) volume 0 (2 * π)

Tactic:
simpa only [tsum_mul_left, tsum_geometric_of_lt_one hwR.1 hwR.2] using
      hf.norm.mul_continuousOn continuousOn_const

Premises used: IntervalIntegrable.mul_continuousOn, continuousOn_const, tsum_geometric_of_lt_one, tsum_mul_left, IntervalIntegrable.norm, And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum
        (fun (n : ℕ) ↦
          HSMul.hSMul (β := E) (deriv (circleMap c R) t)
            ((fun (z : ℂ) ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)))
        (HSMul.hSMul (β := E) (deriv (circleMap c R) t) ((fun (z : ℂ) ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t)))

Tactic:
Eventually.of_forall fun θ _ => HasSum.const_smul _ ?_

Premises used: deriv, circleMap, Filter.Eventually.of_forall, HasSum.const_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
refine_5 :
  ∀ θ ∈ Ι 0 (2 * π),
    HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ (fun (z : ℂ) ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ))
      ((fun (z : ℂ) ↦ (z - (c + w))⁻¹ • f z) (circleMap c R θ))
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum
        (fun (n : ℕ) ↦
          HSMul.hSMul (β := E) (deriv (circleMap c R) t)
            ((fun (z : ℂ) ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)))
        (HSMul.hSMul (β := E) (deriv (circleMap c R) t) ((fun (z : ℂ) ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t)))

Tactic:
refine Eventually.of_forall fun θ _ => HasSum.const_smul _ ?_

Premises used: Filter.Eventually.of_forall, HasSum.const_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
refine_5 :
  HasSum (fun (n : ℕ) ↦ ((w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) • f (circleMap c R θ))
    ((circleMap c R θ - (c + w))⁻¹ • f (circleMap c R θ))
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ (fun (z : ℂ) ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ))
    ((fun (z : ℂ) ↦ (z - (c + w))⁻¹ • f z) (circleMap c R θ))

Tactic:
simp only [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
⊢ HasSum (fun (n : ℕ) ↦ ((w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) • f (circleMap c R θ))
    ((circleMap c R θ - (c + w))⁻¹ • f (circleMap c R θ))

Tactic:
HasSum.smul_const ?_ _

Premises used: HasSum.smul_const
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
refine_5 :
  HasSum (fun (n : ℕ) ↦ (w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) (circleMap c R θ - (c + w))⁻¹
⊢ HasSum (fun (n : ℕ) ↦ ((w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) • f (circleMap c R θ))
    ((circleMap c R θ - (c + w))⁻¹ • f (circleMap c R θ))

Tactic:
refine HasSum.smul_const ?_ _

Premises used: HasSum.smul_const
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
⊢ ‖w / (circleMap c R θ - c)‖ < 1

Tactic:
simpa [abs_of_pos hR] using hwR.2

Premises used: And.right, abs_of_pos
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
⊢ ‖w / (circleMap c R θ - c)‖ < 1

Tactic:
have : ‖w / (circleMap c R θ - c)‖ < 1 := by simpa [abs_of_pos hR] using hwR.2
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
this : ‖w / (circleMap c R θ - c)‖ < 1
⊢ HasSum (fun (i : ℕ) ↦ (w / (circleMap c R θ - c)) ^ i * (circleMap c R θ - c)⁻¹)
    ((1 - w / (circleMap c R θ - c))⁻¹ * (circleMap c R θ - c)⁻¹)

Tactic:
(hasSum_geometric_of_norm_lt_one this).mul_right _

Premises used: hasSum_geometric_of_norm_lt_one, HasSum.mul_right
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
θ : ℝ
h_1 : θ ∈ Ι 0 (2 * π)
this : ‖w / (circleMap c R θ - c)‖ < 1
h : (circleMap c R θ - (c + w))⁻¹ = (1 - w / (circleMap c R θ - c))⁻¹ * (circleMap c R θ - c)⁻¹
⊢ HasSum (fun (n : ℕ) ↦ (w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) (circleMap c R θ - (c + w))⁻¹

Tactic:
convert! (hasSum_geometric_of_norm_lt_one this).mul_right _ using 1

Premises used: hasSum_geometric_of_norm_lt_one, HasSum.mul_right
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
this : ‖w / (circleMap c R θ - c)‖ < 1
⊢ (circleMap c R θ - (c + w))⁻¹ = (1 - w / (circleMap c R θ - c))⁻¹ * (circleMap c R θ - c)⁻¹

Tactic:
simp [← sub_sub, ← mul_inv, sub_mul, div_mul_cancel₀ _ (circleMap_ne_center hR.ne')]

Premises used: div_mul_cancel₀, mul_inv, circleMap_ne_center, LT.lt.ne', sub_mul, sub_sub
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
simp :
  HasSum
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z))
    (HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z))
⊢ HasSum (fun (n : ℕ) ↦ (cauchyPowerSeries f c R n : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ w)
    (HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z))

Tactic:
simp only [cauchyPowerSeries_apply]

Premises used: cauchyPowerSeries_apply
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
⊢ HasSum
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z))
    (HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z))

Tactic:
(hasSum_two_pi_I_cauchyPowerSeries_integral hf hw).const_smul _

Premises used: hasSum_two_pi_I_cauchyPowerSeries_integral, HasSum.const_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
⊢ HasSum
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z))
    (HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z))

Tactic:
exact (hasSum_two_pi_I_cauchyPowerSeries_integral hf hw).const_smul _

Premises used: hasSum_two_pi_I_cauchyPowerSeries_integral, HasSum.const_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
⊢ FormalMultilinearSeries.sum (cauchyPowerSeries f c R) w =
    HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

Tactic:
(hasSum_cauchyPowerSeries_integral hf hw).tsum_eq

Premises used: hasSum_cauchyPowerSeries_integral, HasSum.tsum_eq, FormalMultilinearSeries.sum
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
hf : CircleIntegrable f c (↑R : ℝ)
hR : 0 < R
y : ℂ
hy : Membership.mem (γ := Set ℂ) (eball 0 (↑R : ENNReal)) y
⊢ ‖y‖ < (↑R : ℝ)

Tactic:
simpa using hy
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
⊢ 0 < R

Tactic:
have hR : 0 < R := dist_nonneg.trans_lt hw
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * (↑π : ℂ) * I)
⊢ CircleIntegrable (E := ℂ) (fun (x : ℂ) ↦ 1) c R

Tactic:
have A : CircleIntegrable (fun _ => (1 : ℂ)) c R := continuousOn_const.circleIntegrable'
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * (↑π : ℂ) * I)
A : CircleIntegrable (E := ℂ) (fun (x : ℂ) ↦ 1) c R
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * (↑π : ℂ) * I

Tactic:
(H.unique ?_).symm

Premises used: HasSum.unique, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * (↑π : ℂ) * I)
A : CircleIntegrable (E := ℂ) (fun (x : ℂ) ↦ 1) c R
refine :
  HasSum (α := ℂ) (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹)
    (∮ (z : ℂ) in C(c, R), (z - w)⁻¹)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * (↑π : ℂ) * I

Tactic:
refine (H.unique ?_).symm

Premises used: HasSum.unique, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * (↑π : ℂ) * I)
A : CircleIntegrable (E := ℂ) (fun (x : ℂ) ↦ 1) c R
⊢ HasSum (α := ℂ) (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹)
    (∮ (z : ℂ) in C(c, R), (z - w)⁻¹)

Tactic:
simpa only [smul_eq_mul, mul_one, add_sub_cancel] using
      hasSum_two_pi_I_cauchyPowerSeries_integral A (mem_ball_iff_norm.1 hw)

Premises used: hasSum_two_pi_I_cauchyPowerSeries_integral, mem_ball_iff_norm, add_sub_cancel, Iff.mp, smul_eq_mul, mul_one
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
suffices : HasSum (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * (↑π : ℂ) * I)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * (↑π : ℂ) * I

Tactic:
suffices H : HasSum (fun n : ℕ => ∮ z in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹)
      (2 * π * I) by
    have A : CircleIntegrable (fun _ => (1 : ℂ)) c R := continuousOn_const.circleIntegrable'
    refine (H.unique ?_).symm
    simpa only [smul_eq_mul, mul_one, add_sub_cancel] using
      hasSum_two_pi_I_cauchyPowerSeries_integral A (mem_ball_iff_norm.1 hw)
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ (n : ℕ), n ≠ 0 → Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) 0

Tactic:
fun n hn => integral_sub_zpow_of_ne ?_ _ _ _

Premises used: circleIntegral.integral_sub_zpow_of_ne
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
refine : ∀ (n : ℕ) (hn : n ≠ 0), HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 ≠ -1
⊢ ∀ (n : ℕ), n ≠ 0 → Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) 0

Tactic:
refine fun n hn => integral_sub_zpow_of_ne ?_ _ _ _

Premises used: circleIntegral.integral_sub_zpow_of_ne
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
n : ℕ
hn : n ≠ 0
⊢ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 ≠ -1

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ (n : ℕ), n ≠ 0 → Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) 0

Tactic:
have H : ∀ n : ℕ, n ≠ 0 → (∮ z in C(c, R), (z - c) ^ (-n - 1 : ℤ)) = 0 := by
    refine fun n hn => integral_sub_zpow_of_ne ?_ _ _ _; simpa
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) 0
⊢ ∮ (z : ℂ) in C(c, R), HPow.hPow (β := ℕ) ((w - c) / (z - c)) 0 * (z - c)⁻¹ = 2 * (↑π : ℂ) * I

Tactic:
simp [hR.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) 0
⊢ ∮ (z : ℂ) in C(c, R), HPow.hPow (β := ℕ) ((w - c) / (z - c)) 0 * (z - c)⁻¹ = 2 * (↑π : ℂ) * I

Tactic:
have : (∮ z in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * π * I := by simp [hR.ne']
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) 0
this : ∮ (z : ℂ) in C(c, R), HPow.hPow (β := ℕ) ((w - c) / (z - c)) 0 * (z - c)⁻¹ = 2 * (↑π : ℂ) * I
⊢ HasSum (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * (↑π : ℂ) * I)

Tactic:
this ▸ hasSum_single _ fun n hn => ?_

Premises used: hasSum_single, Eq.rec, SummationFilter.unconditional
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) 0
this : ∮ (z : ℂ) in C(c, R), HPow.hPow (β := ℕ) ((w - c) / (z - c)) 0 * (z - c)⁻¹ = 2 * (↑π : ℂ) * I
refine : ∀ (n : ℕ) (hn : n ≠ 0), Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) 0
⊢ HasSum (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * (↑π : ℂ) * I)

Tactic:
refine this ▸ hasSum_single _ fun n hn => ?_
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) 0
this : ∮ (z : ℂ) in C(c, R), HPow.hPow (β := ℕ) ((w - c) / (z - c)) 0 * (z - c)⁻¹ = 2 * (↑π : ℂ) * I
n : ℕ
hn : n ≠ 0
simp : (w - c) ^ n * ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n * (z - c)⁻¹ = 0
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) 0

Tactic:
simp only [div_eq_mul_inv, mul_pow, integral_const_mul, mul_assoc]

Premises used: mul_assoc, div_eq_mul_inv, mul_pow, circleIntegral.integral_const_mul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) 0
this : ∮ (z : ℂ) in C(c, R), HPow.hPow (β := ℕ) ((w - c) / (z - c)) 0 * (z - c)⁻¹ = 2 * (↑π : ℂ) * I
n : ℕ
hn : n ≠ 0
rw : ∀ (z : ℂ) (hz : z ∈ sphere c R), (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ (w - c) ^ n * ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n * (z - c)⁻¹ = 0

Tactic:
rw [(integral_congr hR.le fun z hz => _).trans (H n hn), mul_zero]

Premises used: circleIntegral.integral_congr, LT.lt.le, MulZeroClass.mul_zero, Eq.trans
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) 0
this : ∮ (z : ℂ) in C(c, R), HPow.hPow (β := ℕ) ((w - c) / (z - c)) 0 * (z - c)⁻¹ = 2 * (↑π : ℂ) * I
n : ℕ
hn : n ≠ 0
z : ℂ
_ : z ∈ sphere c R → (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ ∀ (hz : z ∈ sphere c R), (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1

Tactic:
_