awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z :
  ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ =
    ‖HSub.hSub (α := E) (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y)‖
z₁ :
  ‖HSub.hSub (α := E) (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y)‖ =
    norm.{u} (E := E) (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • (f z - y))
z₂ : norm.{u} (E := E) (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • (f z - y)) ≤ 2 * π * r * (r⁻¹ * (ε / (2 * π)))
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ ε
have z₃ : 2 * π * r * (r⁻¹ * (ε / (2 * π))) = ε
Tactic: calc
    ‖(∮ z in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ =
        ‖(∮ z in C(c, r), (z - c)⁻¹ • f z) - ∮ z in C(c, r), (z - c)⁻¹ • y‖ := by
      congr 2
      · exact circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable hr0
          hrR hs (hc.mono hsub) fun z hz => hd z ⟨hsub' hz.1, hz.2⟩
      · simp [hr0.ne']
    _ = ‖∮ z in C(c, r), (z - c)⁻¹ • (f z - y)‖ := by
      simp only [smul_sub]
      have hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r) :=
        (continuousOn_id.sub continuousOn_const).inv₀ fun z hz => sub_ne_zero.2 <| hzne _ hz
      rw [circleIntegral.integral_sub] <;> refine (hc'.smul ?_).circleIntegrable hr0.le
      · exact hc.mono <| subset_inter
          (sphere_subset_closedBall.trans <| closedBall_subset_closedBall hrR) hzne
      · exact continuousOn_const
    _ ≤ 2 * π * r * (r⁻¹ * (ε / (2 * π))) := by
      refine circleIntegral.norm_integral_le_of_norm_le_const hr0.le fun z hz => ?_
      specialize hzne z hz
      rw [mem_sphere, dist_eq_norm] at hz
      rw [norm_smul, norm_inv, hz, ← dist_eq_norm]
      refine mul_le_mul_of_nonneg_left (hδ _ ⟨?_, hzne⟩).le (inv_nonneg.2 hr0.le)
      rwa [mem_closedBall_iff_norm, hz]
    _ = ε := by field
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
h0 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0
have inr : ∀ (this : ∀ (hE : CompleteSpace E), Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0) (hE : ¬CompleteSpace E),
  Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0
Tactic: wlog hE : CompleteSpace E generalizing
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
h0 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
inr :
  ∀ (this : ∀ (hE : CompleteSpace E), Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0) (hE : ¬CompleteSpace E),
    Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0
have wlog : ∀ (hE : CompleteSpace E), Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0
Tactic: wlog hE : CompleteSpace E generalizing
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
h0 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
hE : CompleteSpace E
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0
have inl : ∀ (h0 : LE.le (α := ℝ) 0 0) (hc : ContinuousOn f (closedBall c 0)) (hd : ∀ z ∈ ball c 0 \ s, DifferentiableAt ℂ f z),
  Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, 0), f z) 0
Tactic: rcases h0.eq_or_lt with (rfl | h0)
Cleared hypotheses: R, h0, hc, hd
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
h0 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
hE : CompleteSpace E
inl :
  ∀ (h0 : LE.le (α := ℝ) 0 0) (hc : ContinuousOn f (closedBall c 0)) (hd : ∀ z ∈ ball c 0 \ s, DifferentiableAt ℂ f z),
    Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, 0), f z) 0
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0
have inr : ∀ (h0 : 0 < R), Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0
Tactic: rcases h0.eq_or_lt with (rfl | h0)
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
h0_1 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
hE : CompleteSpace E
h0 : 0 < R
⊢ (2 * (↑π : ℂ) * I) • (c - c) • f c = 0
have rw : (2 * (↑π : ℂ) * I) • HSMul.hSMul (α := ℂ) 0 (f c) = 0
Tactic: rw [sub_self, zero_smul, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
h0_1 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
hE : CompleteSpace E
h0 : 0 < R
rw : (2 * (↑π : ℂ) * I) • HSMul.hSMul (α := ℂ) 0 (f c) = 0
⊢ (2 * (↑π : ℂ) * I) • (c - c) • f c = 0
have rw₁ : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I) 0 = 0
Tactic: rw [sub_self, zero_smul, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
h0_1 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
hE : CompleteSpace E
h0 : 0 < R
rw : (2 * (↑π : ℂ) * I) • HSMul.hSMul (α := ℂ) 0 (f c) = 0
rw₁ : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I) 0 = 0
⊢ (2 * (↑π : ℂ) * I) • (c - c) • f c = 0
have rw₂ : Eq.{u + 1} (α := E) 0 0
Tactic: rw [sub_self, zero_smul, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
h0_1 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
hE : CompleteSpace E
h0 : 0 < R
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0
have z : (2 * (↑π : ℂ) * I) • (c - c) • f c = 0
Tactic: calc
    (∮ z in C(c, R), f z) = ∮ z in C(c, R), (z - c)⁻¹ • (z - c) • f z :=
      (circleIntegral.integral_sub_inv_smul_sub_smul _ _ _ _).symm
    _ = (2 * ↑π * I : ℂ) • (c - c) • f c :=
      (circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable h0 hs
        ((continuousOn_id.sub continuousOn_const).smul hc) fun z hz =>
        (differentiableAt_id.sub_const _).smul (hd z hz))
    _ = 0 := by rw [sub_self, zero_smul, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w
have hR : 0 < R
Tactic: have hR : 0 < R := dist_nonneg.trans_lt hw.1
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w
have hws : (insert w s).Countable
Tactic: have hws : (insert w s).Countable := hs.insert w
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w
have hcF : ContinuousOn F (closedBall c R)
Tactic: have hcF : ContinuousOn F (closedBall c R) :=
    (continuousOn_dslope <| closedBall_mem_nhds_of_mem hw.1).2 ⟨hc, hd _ hw⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w
have hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
Tactic: have hdF : ∀ z ∈ ball (c : ℂ) R \ insert w s, DifferentiableAt ℂ F z := fun z hz =>
    (differentiableAt_dslope_of_ne (ne_of_mem_of_not_mem (mem_insert _ _) hz.2).symm).2
      (hd _ (diff_subset_diff_right (subset_insert _ _) hz))
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w
have HI : Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), F z) 0
Tactic: have HI := circleIntegral_eq_zero_of_differentiable_on_off_countable hR.le hws hcF hdF
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), F z) 0
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w
have hne : ∀ z ∈ sphere c R, z ≠ w
Tactic: have hne : ∀ z ∈ sphere c R, z ≠ w := fun z hz => ne_of_mem_of_not_mem hz (ne_of_lt hw.1)
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), F z) 0
hne : ∀ z ∈ sphere c R, z ≠ w
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w
have hFeq : EqOn F (fun (z : ℂ) ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
Tactic: have hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R) := fun z hz ↦
    calc
      F z = (z - w)⁻¹ • (f z - f w) := update_of_ne (hne z hz) ..
      _ = (z - w)⁻¹ • f z - (z - w)⁻¹ • f w := smul_sub _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), F z) 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun (z : ℂ) ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w
have hc' : ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (z - w)⁻¹) (sphere c R)
Tactic: have hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R) :=
    (continuousOn_id.sub continuousOn_const).inv₀ fun z hz => sub_ne_zero.2 <| hne z hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), F z) 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun (z : ℂ) ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (z - w)⁻¹) (sphere c R)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w
have hf : CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (z - w)⁻¹ • f z) c R
Tactic: rw [← circleIntegral.integral_sub_inv_of_mem_ball hw.1, ← circleIntegral.integral_smul_const, ←
    sub_eq_zero, ← circleIntegral.integral_sub, ← circleIntegral.integral_congr hR.le hFeq, HI]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), F z) 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun (z : ℂ) ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (z - w)⁻¹) (sphere c R)
hf : CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (z - w)⁻¹ • f z) c R
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w
have hg : CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (z - w)⁻¹ • f w) c R
Tactic: rw [← circleIntegral.integral_sub_inv_of_mem_ball hw.1, ← circleIntegral.integral_smul_const, ←
    sub_eq_zero, ← circleIntegral.integral_sub, ← circleIntegral.integral_congr hR.le hFeq, HI]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
have hR : 0 < R
Tactic: have hR : 0 < R := dist_nonneg.trans_lt hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
this : w ∈ closure (ball c R \ s)
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
have lift : ∀ (R : ℝ≥0) (hw : w ∈ ball c (↑R : ℝ)) (hc : ContinuousOn f (closedBall c (↑R : ℝ)))
  (hd : ∀ x ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f x) (hR : 0 < (↑R : ℝ))
  (this : w ∈ closure (ball c (↑R : ℝ) \ s)),
  HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z) = f w
Tactic: lift R to ℝ≥0 using hR.le
Cleared hypotheses: R, hw, hc, hd, hR, this
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c (↑R : ℝ)
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ x ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f x
hR : 0 < (↑R : ℝ)
this : w ∈ closure (ball c (↑R : ℝ) \ s)
⊢ ContinuousAt.{0, u} (Y := E)
    (fun (w : ℂ) ↦ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z)) w
have this₁ : HasFPowerSeriesOnBall
  (fun (w : ℂ) ↦ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z))
  (cauchyPowerSeries f c (↑R : ℝ)) c (↑R : ℝ≥0∞)
Tactic: have := hasFPowerSeriesOn_cauchy_integral
        ((hc.mono sphere_subset_closedBall).circleIntegrable R.coe_nonneg) hR
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c (↑R : ℝ)
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ x ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f x
hR : 0 < (↑R : ℝ)
this_1 : w ∈ closure (ball c (↑R : ℝ) \ s)
this :
  HasFPowerSeriesOnBall
    (fun (w : ℂ) ↦ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z))
    (cauchyPowerSeries f c (↑R : ℝ)) c (↑R : ℝ≥0∞)
⊢ ContinuousAt.{0, u} (Y := E)
    (fun (w : ℂ) ↦ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z)) w
have refine : w ∈ eball c (↑R : ℝ≥0∞)
Tactic: refine this.continuousOn.continuousAt (Metric.isOpen_eball.mem_nhds ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c (↑R : ℝ)
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ x ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f x
hR : 0 < (↑R : ℝ)
this : w ∈ closure (ball c (↑R : ℝ) \ s)
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z) = f w
have A : ContinuousAt.{0, u} (Y := E)
  (fun (w : ℂ) ↦ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z)) w
Tactic: have A : ContinuousAt (fun w => (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) w := by
      have := hasFPowerSeriesOn_cauchy_integral
        ((hc.mono sphere_subset_closedBall).circleIntegrable R.coe_nonneg) hR
      refine this.continuousOn.continuousAt (Metric.isOpen_eball.mem_nhds ?_)
      rwa [Metric.eball_coe]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c (↑R : ℝ)
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ x ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f x
hR : 0 < (↑R : ℝ)
this : w ∈ closure (ball c (↑R : ℝ) \ s)
A :
  ContinuousAt.{0, u} (Y := E)
    (fun (w : ℂ) ↦ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z)) w
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z) = f w
have B : ContinuousAt f w
Tactic: have B : ContinuousAt f w := hc.continuousAt (closedBall_mem_nhds_of_mem hw)
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c (↑R : ℝ)
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ x ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f x
hR : 0 < (↑R : ℝ)
this : w ∈ closure (ball c (↑R : ℝ) \ s)
A :
  ContinuousAt.{0, u} (Y := E)
    (fun (w : ℂ) ↦ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z)) w
B : ContinuousAt f w
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z) = f w
have refine : ∀ x ∈ ball c (↑R : ℝ) \ s,
  HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - x)⁻¹ • f z) = f x
Tactic: refine tendsto_nhds_unique_of_frequently_eq A B ((mem_closure_iff_frequently.1 this).mono ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c (↑R : ℝ)
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ x ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f x
hR : 0 < (↑R : ℝ)
this : w ∈ closure (ball c (↑R : ℝ) \ s)
A :
  ContinuousAt.{0, u} (Y := E)
    (fun (w : ℂ) ↦ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z)) w
B : ContinuousAt f w
z : ℂ
hz : z ∈ ball c (↑R : ℝ) \ s
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z_1 : ℂ) in C(c, (↑R : ℝ)), (z_1 - z)⁻¹ • f z_1) = f z
have ha : 2 * (↑π : ℂ) * I ≠ 0
Tactic: rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux hs hz hc hd,
      inv_smul_smul₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
have suffices : w ∈ closure (ball c R \ s)
Tactic: suffices w ∈ closure (ball c R \ s) by
    lift R to ℝ≥0 using hR.le
    have A : ContinuousAt (fun w => (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) w := by
      have := hasFPowerSeriesOn_cauchy_integral
        ((hc.mono sphere_subset_closedBall).circleIntegrable R.coe_nonneg) hR
      refine this.continuousOn.continuousAt (Metric.isOpen_eball.mem_nhds ?_)
      rwa [Metric.eball_coe]
    have B : ContinuousAt f w := hc.continuousAt (closedBall_mem_nhds_of_mem hw)
    refine tendsto_nhds_unique_of_frequently_eq A B ((mem_closure_iff_frequently.1 this).mono ?_)
    intro z hz
    rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux hs hz hc hd,
      inv_smul_smul₀]
    simp [Real.pi_ne_zero, I_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
⊢ w ∈ closure (ball c R \ s)
have refine : ∀ (t : Set ℂ) (ht : t ∈ 𝓝 w), (t ∩ (ball c R \ s)).Nonempty
Tactic: refine mem_closure_iff_nhds.2 fun t ht => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
⊢ (t ∩ (ball c R \ s)).Nonempty
have this : Tendsto g (𝓝 0) (𝓝 w)
Tactic: have : Tendsto g (𝓝 0) (𝓝 w) := Continuous.tendsto' (by fun_prop) 0 w (add_zero _)