awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
have pos : ∀ (H : w ∈ sphere c |R| ∧ n < -1), Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
Tactic: by_cases! H : w ∈ sphere c |R| ∧ n < -1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
have neg : ∀ (H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n), Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
Tactic: by_cases! H : w ∈ sphere c |R| ∧ n < -1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| ∧ n < -1
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
have hw : w ∈ sphere c |R|
Tactic: rcases H with ⟨hw, hn⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| ∧ n < -1
hw : w ∈ sphere c |R|
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
have hn₁ : n < -1
Tactic: rcases H with ⟨hw, hn⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ HasDerivAt (fun (z : ℂ) ↦ (z - w) ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ((z - w) ^ n) z
have h : (z - w) ^ n = (↑(n + 1) : ℂ) * (id z - w) ^ (n + 1 - 1) * 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
Tactic: convert!
      ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const
        _ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
h : (z - w) ^ n = (↑(n + 1) : ℂ) * (id z - w) ^ (n + 1 - 1) * 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
⊢ HasDerivAt (fun (z : ℂ) ↦ (z - w) ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ((z - w) ^ n) z
have convert_1 : z ≠ w → id z - w ≠ 0
Tactic: convert!
      ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const
        _ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
h : (z - w) ^ n = (↑(n + 1) : ℂ) * (id z - w) ^ (n + 1 - 1) * 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
convert_1 : z ≠ w → id z - w ≠ 0
⊢ HasDerivAt (fun (z : ℂ) ↦ (z - w) ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ((z - w) ^ n) z
have convert_2 : -1 ≤ n → 0 ≤ n + 1
Tactic: convert!
      ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const
        _ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
have rwa : ¬HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = 0
Tactic: rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
rwa : ¬HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = 0
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
have rwa₁ : ¬Eq (α := ℂ) (↑n : ℂ) (-1)
Tactic: rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
rwa : ¬HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = 0
rwa₁ : ¬Eq (α := ℂ) (↑n : ℂ) (-1)
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
have rwa₂ : ¬Eq (α := ℂ) (↑n : ℂ) (-(↑1 : ℂ))
Tactic: rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
rwa : ¬HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = 0
rwa₁ : ¬Eq (α := ℂ) (↑n : ℂ) (-1)
rwa₂ : ¬Eq (α := ℂ) (↑n : ℂ) (-(↑1 : ℂ))
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
have rwa₃ : ¬Eq (α := ℂ) (↑n : ℂ) (↑(-1) : ℂ)
Tactic: rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
rwa : ¬HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = 0
rwa₁ : ¬Eq (α := ℂ) (↑n : ℂ) (-1)
rwa₂ : ¬Eq (α := ℂ) (↑n : ℂ) (-(↑1 : ℂ))
rwa₃ : ¬Eq (α := ℂ) (↑n : ℂ) (↑(-1) : ℂ)
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
have rwa₄ : ¬n = -1
Tactic: rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ (z - w) ^ n = (↑(n + 1) : ℂ) * (id z - w) ^ (n + 1 - 1) * 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
have hn' : HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
Tactic: have hn' : (n + 1 : ℂ) ≠ 0 := by
        rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
have hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun (z : ℂ) ↦ (z - w) ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ((z - w) ^ n) z
Tactic: have hd : ∀ z, z ≠ w ∨ -1 ≤ n →
      HasDerivAt (fun z => (z - w) ^ (n + 1) / (n + 1)) ((z - w) ^ n) z := by
    intro z hne
    convert!
      ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const
        _ using 1
    · have hn' : (n + 1 : ℂ) ≠ 0 := by
        rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
      simp [mul_div_cancel_left₀ _ hn']
    exacts [sub_ne_zero.2, neg_le_iff_add_nonneg.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
hd :
  ∀ (z : ℂ),
    z ≠ w ∨ -1 ≤ n → HasDerivAt (fun (z : ℂ) ↦ (z - w) ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ((z - w) ^ n) z
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
have neg : ∀ (z : ℂ) (hz : z ∈ sphere c |R|), z ≠ w ∨ -1 ≤ n
Tactic: refine integral_eq_zero_of_hasDerivWithinAt' fun z hz => (hd z ?_).hasDerivWithinAt
-- 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 : ℝ
n : ℕ
w : ℂ
⊢ ((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), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
have simp : w ^ n • HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) =
  (2 * (↑π : ℂ) * I)⁻¹ • HSMul.hSMul (β := E) (w ^ n) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
Tactic: simp only [cauchyPowerSeries, ContinuousMultilinearMap.mkPiRing_apply, Fin.prod_const,
    div_eq_mul_inv, mul_pow, mul_smul, circleIntegral.integral_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 : ℝ
n : ℕ
w : ℂ
⊢ w ^ n • HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) =
    (2 * (↑π : ℂ) * I)⁻¹ • HSMul.hSMul (β := E) (w ^ n) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
have rw : w ^ n • HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) =
  w ^ n • HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
Tactic: rw [← smul_comm (w ^ 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 : ℝ
n : ℕ
⊢ (2 * π)⁻¹ * norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) ≤
    (2 * π)⁻¹ *
      ∫ (θ : ℝ) in 0..2 * π,
        ‖deriv (circleMap c R) θ • (circleMap c R θ - c)⁻¹ ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ)‖
have hbc : norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) ≤
  ∫ (θ : ℝ) in 0..2 * π,
    ‖deriv (circleMap c R) θ • (circleMap c R θ - c)⁻¹ ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ)‖
Tactic: gcongr
-- 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 : ℝ
n : ℕ
⊢ (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n
have inl : (2 * π)⁻¹ *
    (HPow.hPow (α := ℝ) |0|⁻¹ n * (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
  ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) |0|⁻¹ n
Tactic: rcases eq_or_ne R 0 with (rfl | hR)
Cleared hypotheses: R
-- 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 : ℝ
n : ℕ
inl :
  (2 * π)⁻¹ *
      (HPow.hPow (α := ℝ) |0|⁻¹ n * (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) |0|⁻¹ n
⊢ (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n
have inr : ∀ (hR : R ≠ 0),
  (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n
Tactic: rcases eq_or_ne R 0 with (rfl | hR)
-- 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 : ℂ
n : ℕ
⊢ (2 * π)⁻¹ *
      (HPow.hPow (α := ℝ) |0|⁻¹ n * (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) |0|⁻¹ n
have inl : (2 * π)⁻¹ *
    (HPow.hPow (α := ℝ) (β := ℕ) |0|⁻¹ 0 *
      (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
  ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) (β := ℕ) |0|⁻¹ 0
Tactic: cases n
Cleared hypotheses: 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 : ℂ
n : ℕ
inl :
  (2 * π)⁻¹ *
      (HPow.hPow (α := ℝ) (β := ℕ) |0|⁻¹ 0 *
        (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) (β := ℕ) |0|⁻¹ 0
⊢ (2 * π)⁻¹ *
      (HPow.hPow (α := ℝ) |0|⁻¹ n * (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) |0|⁻¹ n
have inl₁ : ∀ (n : ℕ),
  (2 * π)⁻¹ *
      (HPow.hPow (α := ℝ) |0|⁻¹ (n + 1) *
        (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) |0|⁻¹ (n + 1)
Tactic: cases n
Cleared hypotheses: 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 : ℝ
n : ℕ
hR : R ≠ 0
⊢ (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n
have inr : |R| ≠ 0
Tactic: rw [mul_inv_cancel_left₀, mul_assoc, mul_comm (|R|⁻¹ ^ 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 : ℝ
n : ℕ
hR : R ≠ 0
⊢ |R| ≠ 0
have inr : ¬|R| = 0
Tactic: rwa [Ne, _root_.abs_eq_zero]
-- 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 : ℝ
n : ℕ
hR : R ≠ 0
inr : ¬|R| = 0
⊢ |R| ≠ 0
have inr₁ : ¬R = 0
Tactic: rwa [Ne, _root_.abs_eq_zero]
-- 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 : ℝ≥0
⊢ (↑R : ENNReal) ≤ FormalMultilinearSeries.radius (cauchyPowerSeries f c (↑R : ℝ))
have f₁ : ∀ (n : ℕ),
  norm (E := ContinuousMultilinearMap ℂ (fun (i : Fin n) ↦ ℂ) E) (cauchyPowerSeries f c (↑R : ℝ) n) * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
Tactic: refine
    (cauchyPowerSeries f c R).le_radius_of_bound
      ((2 * π)⁻¹ * ∫ θ : ℝ in 0..2 * π, ‖f (circleMap c R θ)‖) 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 : ℝ≥0
n : ℕ
⊢ norm (E := ContinuousMultilinearMap ℂ (fun (i : Fin n) ↦ ℂ) E) (cauchyPowerSeries f c (↑R : ℝ) n) * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
have refine : ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * |(↑R : ℝ)|⁻¹ ^ n * (↑R : ℝ) ^ n ≤
  (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
Tactic: refine (mul_le_mul_of_nonneg_right (norm_cauchyPowerSeries_le _ _ _ _)
    (pow_nonneg R.coe_nonneg _)).trans ?_
-- 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 : ℝ≥0
n : ℕ
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * |(↑R : ℝ)|⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
have rw : ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
  (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
Tactic: rw [abs_of_nonneg R.coe_nonneg]
-- 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 : ℝ≥0
n : ℕ
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
have inl : ∀ (hR : (↑R : ℝ) ^ n = 0),
  ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
Tactic: rcases eq_or_ne (R ^ n : ℝ) 0 with hR | hR
-- 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 : ℝ≥0
n : ℕ
inl :
  ∀ (hR : (↑R : ℝ) ^ n = 0),
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
      (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
have inr : ∀ (hR : (↑R : ℝ) ^ n ≠ 0),
  ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
Tactic: rcases eq_or_ne (R ^ n : ℝ) 0 with hR | hR
-- 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 : ℝ≥0
n : ℕ
hR : (↑R : ℝ) ^ n = 0
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
have inl : ∀ (hR : R ^ n = 0), 0 ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
Tactic: rw_mod_cast [hR, mul_zero]
Cleared hypotheses: hR
-- 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 : ℝ≥0
n : ℕ
hR : (↑R : ℝ) ^ n ≠ 0
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
have inr : ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * ((↑R : ℝ) ^ n)⁻¹ * (↑R : ℝ) ^ n ≤
  (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
Tactic: rw [inv_pow]
-- 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 : ℝ≥0
n : ℕ
hR : (↑R : ℝ) ^ n ≠ 0
⊢ (↑R : ℝ) ^ n ≠ 0
have norm_cast : ∀ (hR : ¬R ^ n = 0), ¬R ^ n = 0
Tactic: norm_cast at hR ⊢
Cleared hypotheses: hR
-- 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 : ℝ≥0
n : ℕ
hR this : (↑R : ℝ) ^ n ≠ 0
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * ((↑R : ℝ) ^ n)⁻¹ * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
have inr : (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖ ≤
  (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
Tactic: rw [inv_mul_cancel_right₀ this]
-- 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
⊢ 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 hR : 0 < R
Tactic: have hR : 0 < R := (norm_nonneg w).trans_lt hw
-- 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
⊢ 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 hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
Tactic: have hwR : ‖w‖ / R ∈ Ico (0 : ℝ) 1 :=
    ⟨div_nonneg (norm_nonneg w) hR.le, (div_lt_one hR).2 hw⟩
-- 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)
⊢ 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_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 * π)))
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)
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 * π)))
⊢ 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_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
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)
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
⊢ 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_3 : ∀ᵐ (t : ℝ),
  t ∈ Ι 0 (2 * π) → Summable (α := ℝ) fun (n : ℕ) ↦ (fun (n : ℕ) (θ : ℝ) ↦ ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) n 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)
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
⊢ 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_4 : IntervalIntegrable (ε := ℝ)
  (fun (t : ℝ) ↦ ∑' (n : ℕ), (fun (n : ℕ) (θ : ℝ) ↦ ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) n t) volume 0 (2 * π)
Tactic: refine intervalIntegral.hasSum_integral_of_dominated_convergence
      (fun n θ => ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) (fun n => ?_) (fun n => ?_) ?_ ?_ ?_