awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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_1 :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace)
      (fun (θ : ℝ) ↦
        HSMul.hSMul (β := E) (deriv (circleMap c R) θ)
          ((fun (z : ℂ) ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ)))
      (Measure.restrict volume (Ι 0 (2 * π)))
refine_2 :
  ∀ (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
refine_3 :
  ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) → Summable (α := ℝ) fun (n : ℕ) ↦ (fun (n : ℕ) (θ : ℝ) ↦ ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) n t
refine_4 :
  IntervalIntegrable (ε := ℝ)
    (fun (t : ℝ) ↦ ∑' (n : ℕ), (fun (n : ℕ) (θ : ℝ) ↦ ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) n t) volume 0 (2 * π)
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
have refine_5 : ∀ᵐ (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 intervalIntegral.hasSum_integral_of_dominated_convergence
      (fun n θ => ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) (fun n => ?_) (fun n => ?_) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℕ
⊢ AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace)
    (fun (θ : ℝ) ↦
      HSMul.hSMul (β := E) (deriv (circleMap c R) θ)
        ((fun (z : ℂ) ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ)))
    (Measure.restrict volume (Ι 0 (2 * π)))
have refine_1 : 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: simp only [deriv_circleMap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℕ
⊢ 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 * π)))
have refine_1 : AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ circleMap 0 R x * I)
  (Measure.restrict volume (Ι 0 (2 * π)))
Tactic: apply_rules [AEStronglyMeasurable.smul, hf.def'.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 * π)))
⊢ 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 * π)))
have refine_1₁ : AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ (w / (circleMap c R x - c)) ^ n)
  (Measure.restrict volume (Ι 0 (2 * π)))
Tactic: apply_rules [AEStronglyMeasurable.smul, hf.def'.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 * π)))
⊢ 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 * π)))
have refine_1₂ : AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ (circleMap c R x - c)⁻¹)
  (Measure.restrict volume (Ι 0 (2 * π)))
Tactic: apply_rules [AEStronglyMeasurable.smul, hf.def'.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℕ
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ circleMap 0 R x * I)
    (Measure.restrict volume (Ι 0 (2 * π)))
have refine_1 : Measurable (β := ℂ) fun (x : ℝ) ↦ circleMap 0 R x * I
Tactic: apply Measurable.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℕ
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ (w / (circleMap c R x - c)) ^ n)
    (Measure.restrict volume (Ι 0 (2 * π)))
have refine_1 : Measurable (β := ℂ) fun (x : ℝ) ↦ (w / (circleMap c R x - c)) ^ n
Tactic: apply Measurable.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℕ
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ (circleMap c R x - c)⁻¹)
    (Measure.restrict volume (Ι 0 (2 * π)))
have refine_1 : Measurable (β := ℂ) fun (x : ℝ) ↦ (circleMap c R x - c)⁻¹
Tactic: apply Measurable.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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)))
have 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 θ))
Tactic: refine Eventually.of_forall fun θ _ => HasSum.const_smul _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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.{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 θ))
have 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 θ))
Tactic: simp only [smul_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 θ))
have refine_5 : HasSum (fun (n : ℕ) ↦ (w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) (circleMap c R θ - (c + w))⁻¹
Tactic: refine HasSum.smul_const ?_ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
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)⁻¹) (circleMap c R θ - (c + w))⁻¹
have this : ‖w / (circleMap c R θ - c)‖ < 1
Tactic: have : ‖w / (circleMap c R θ - c)‖ < 1 := by simpa [abs_of_pos hR] using hwR.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 (n : ℕ) ↦ (w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) (circleMap c R θ - (c + w))⁻¹
have h : (circleMap c R θ - (c + w))⁻¹ = (1 - w / (circleMap c R θ - c))⁻¹ * (circleMap c R θ - c)⁻¹
Tactic: convert! (hasSum_geometric_of_norm_lt_one this).mul_right _ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℕ) ↦ (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))
have 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))
Tactic: simp only [cauchyPowerSeries_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * (↑π : ℂ) * I
have hR : 0 < R
Tactic: have hR : 0 < R := dist_nonneg.trans_lt hw
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
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)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * (↑π : ℂ) * I
have A : CircleIntegrable (E := ℂ) (fun (x : ℂ) ↦ 1) c R
Tactic: have A : CircleIntegrable (fun _ => (1 : ℂ)) c R := continuousOn_const.circleIntegrable'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
have refine : HasSum (α := ℂ) (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹)
  (∮ (z : ℂ) in C(c, R), (z - w)⁻¹)
Tactic: refine (H.unique ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * (↑π : ℂ) * I
have suffices : HasSum (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
have refine : ∀ (n : ℕ) (hn : n ≠ 0), HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 ≠ -1
Tactic: refine fun n hn => integral_sub_zpow_of_ne ?_ _ _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ HasSum (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * (↑π : ℂ) * I)
have H : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
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
⊢ HasSum (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * (↑π : ℂ) * I)
have this : ∮ (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']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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)
have refine : ∀ (n : ℕ) (hn : n ≠ 0), Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) 0
Tactic: refine this ▸ hasSum_single _ fun n hn => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) 0
have simp : (w - c) ^ n * ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n * (z - c)⁻¹ = 0
Tactic: simp only [div_eq_mul_inv, mul_pow, integral_const_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
⊢ (w - c) ^ n * ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n * (z - c)⁻¹ = 0
have rw : ∀ (z : ℂ) (hz : z ∈ sphere c R), (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
Tactic: rw [(integral_congr hR.le fun z hz => _).trans (H n hn), mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℂ
hz : z ∈ sphere c R
⊢ (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have rw : (z - c)⁻¹ ^ (n + 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
Tactic: rw [← pow_succ, ← zpow_natCast, inv_zpow, ← zpow_neg, Int.natCast_succ, neg_add,
    sub_eq_add_neg _ (1 : ℤ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℂ
hz : z ∈ sphere c R
rw : (z - c)⁻¹ ^ (n + 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have rw₁ : HPow.hPow (β := ℤ) (z - c)⁻¹ (↑(n + 1) : ℤ) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
Tactic: rw [← pow_succ, ← zpow_natCast, inv_zpow, ← zpow_neg, Int.natCast_succ, neg_add,
    sub_eq_add_neg _ (1 : ℤ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℂ
hz : z ∈ sphere c R
rw : (z - c)⁻¹ ^ (n + 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₁ : HPow.hPow (β := ℤ) (z - c)⁻¹ (↑(n + 1) : ℤ) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have rw₂ : (HPow.hPow (β := ℤ) (z - c) (↑(n + 1) : ℤ))⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
Tactic: rw [← pow_succ, ← zpow_natCast, inv_zpow, ← zpow_neg, Int.natCast_succ, neg_add,
    sub_eq_add_neg _ (1 : ℤ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℂ
hz : z ∈ sphere c R
rw : (z - c)⁻¹ ^ (n + 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₁ : HPow.hPow (β := ℤ) (z - c)⁻¹ (↑(n + 1) : ℤ) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₂ : (HPow.hPow (β := ℤ) (z - c) (↑(n + 1) : ℤ))⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have rw₃ : HPow.hPow (β := ℤ) (z - c) (-(↑(n + 1) : ℤ)) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
Tactic: rw [← pow_succ, ← zpow_natCast, inv_zpow, ← zpow_neg, Int.natCast_succ, neg_add,
    sub_eq_add_neg _ (1 : ℤ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℂ
hz : z ∈ sphere c R
rw : (z - c)⁻¹ ^ (n + 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₁ : HPow.hPow (β := ℤ) (z - c)⁻¹ (↑(n + 1) : ℤ) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₂ : (HPow.hPow (β := ℤ) (z - c) (↑(n + 1) : ℤ))⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₃ : HPow.hPow (β := ℤ) (z - c) (-(↑(n + 1) : ℤ)) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have rw₄ : (z - c) ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
Tactic: rw [← pow_succ, ← zpow_natCast, inv_zpow, ← zpow_neg, Int.natCast_succ, neg_add,
    sub_eq_add_neg _ (1 : ℤ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℂ
hz : z ∈ sphere c R
rw : (z - c)⁻¹ ^ (n + 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₁ : HPow.hPow (β := ℤ) (z - c)⁻¹ (↑(n + 1) : ℤ) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₂ : (HPow.hPow (β := ℤ) (z - c) (↑(n + 1) : ℤ))⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₃ : HPow.hPow (β := ℤ) (z - c) (-(↑(n + 1) : ℤ)) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₄ : (z - c) ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have rw₅ : (z - c) ^ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
Tactic: rw [← pow_succ, ← zpow_natCast, inv_zpow, ← zpow_neg, Int.natCast_succ, neg_add,
    sub_eq_add_neg _ (1 : ℤ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 : ℂ
hz : z ∈ sphere c R
rw : (z - c)⁻¹ ^ (n + 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₁ : HPow.hPow (β := ℤ) (z - c)⁻¹ (↑(n + 1) : ℤ) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₂ : (HPow.hPow (β := ℤ) (z - c) (↑(n + 1) : ℤ))⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₃ : HPow.hPow (β := ℤ) (z - c) (-(↑(n + 1) : ℤ)) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₄ : (z - c) ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₅ : (z - c) ^ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have rw₆ : (z - c) ^ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1) = (z - c) ^ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1)
Tactic: rw [← pow_succ, ← zpow_natCast, inv_zpow, ← zpow_neg, Int.natCast_succ, neg_add,
    sub_eq_add_neg _ (1 : ℤ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ Periodic (circleTransformDeriv R z w f) (2 * π)
have this : ∀ (c : ℂ) (R : ℝ), Periodic (circleMap c R) (2 * π)
Tactic: have := periodic_circleMap
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ circleTransformDeriv R z w f (x + 2 * π) = circleTransformDeriv R z w f x
have simp_rw : (2 * (↑π : ℂ) * I)⁻¹ •
    deriv (circleMap z R) (x + 2 * π) • (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹ • f (circleMap z R x) =
  (2 * (↑π : ℂ) * I)⁻¹ • deriv (circleMap z R) x • (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹ • f (circleMap z R x)
Tactic: simp_rw [circleTransformDeriv, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ (2 * (↑π : ℂ) * I)⁻¹ •
      deriv (circleMap z R) (x + 2 * π) • (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹ • f (circleMap z R x) =
    (2 * (↑π : ℂ) * I)⁻¹ •
      deriv (circleMap z R) x • (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹ • f (circleMap z R x)
have e_a : deriv (circleMap z R) (x + 2 * π) = deriv (circleMap z R) x
Tactic: congr 2