awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
inr : ∀ (h0 : 0 < R), Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0

Tactic:
rcases h0.eq_or_lt with (rfl | h0)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hE : CompleteSpace E
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:
apply circleIntegral.integral_radius_zero

Premises used: circleIntegral.integral_radius_zero
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • (z - c) • f z)

Tactic:
(circleIntegral.integral_sub_inv_smul_sub_smul _ _ _ _).symm

Premises used: circleIntegral.integral_sub_inv_smul_sub_smul, Eq.symm
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • (z - c) • f z = (2 * (↑π : ℂ) * I) • (c - c) • f c

Tactic:
(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))

Premises used: Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable, DifferentiableAt.smul, ContinuousOn.sub, continuousOn_const, ContinuousOn.smul, continuousOn_id
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
rw₂ rw₃ : Eq.{u + 1} (α := E) 0 0
⊢ (2 * (↑π : ℂ) * I) • (c - c) • f c = 0

Tactic:
rw [sub_self, zero_smul, smul_zero]

Premises used: sub_self, smul_zero, zero_smul
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
z : (2 * (↑π : ℂ) * I) • (c - c) • f c = 0
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 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]

Premises used: HMul.hMul, Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable, circleIntegral.integral_sub_inv_smul_sub_smul, DifferentiableAt.smul, HSub.hSub, ContinuousOn.sub, continuousOn_const, ContinuousOn.smul, circleIntegral, continuousOn_id, OfNat.ofNat, Eq.symm, Complex.I
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
h0 : 0 ≤ R
f : ℂ → E
c : ℂ
hc : DiffContOnCl ℂ f (ball c R)
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0

Tactic:
circleIntegral_eq_zero_of_differentiable_on_off_countable h0 countable_empty
    hc.continuousOn_ball fun _z hz ↦ hc.differentiableAt isOpen_ball hz.1

Premises used: DiffContOnCl.continuousOn_ball, Metric.isOpen_ball, And.left, DiffContOnCl.differentiableAt, Complex.circleIntegral_eq_zero_of_differentiable_on_off_countable, Set.countable_empty
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ 0 < R

Tactic:
have hR : 0 < R := dist_nonneg.trans_lt hw.1
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ (insert w s).Countable

Tactic:
have hws : (insert w s).Countable := hs.insert w
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ 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⟩
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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 ∈ 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))
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ 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
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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 ∈ 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)
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ 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 _ _ _
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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)
⊢ 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
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
hg : CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (z - w)⁻¹ • f w) c R
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w

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]

Premises used: circleIntegral.integral_sub_inv_of_mem_ball, sub_eq_zero, circleIntegral.integral_congr, LT.lt.le, circleIntegral.integral_sub, And.left, circleIntegral.integral_smul_const
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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)
⊢ CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (z - w)⁻¹ • f z) c R

Tactic:
(hc'.smul (hc.mono sphere_subset_closedBall)).circleIntegrable hR.le

Premises used: ContinuousOn.circleIntegrable, LT.lt.le, ContinuousOn.smul, ContinuousOn.mono, Metric.sphere_subset_closedBall
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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)
⊢ CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (z - w)⁻¹ • f w) c R

Tactic:
(hc'.smul continuousOn_const).circleIntegrable hR.le

Premises used: ContinuousOn.circleIntegrable, continuousOn_const, LT.lt.le, ContinuousOn.smul
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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)
⊢ CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (z - w)⁻¹ • f z) c R

Tactic:
exacts [(hc'.smul (hc.mono sphere_subset_closedBall)).circleIntegrable hR.le,
    (hc'.smul continuousOn_const).circleIntegrable hR.le]

Premises used: ContinuousOn.circleIntegrable, continuousOn_const, LT.lt.le, ContinuousOn.smul, ContinuousOn.mono, Metric.sphere_subset_closedBall
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ 0 < R

Tactic:
have hR : 0 < R := dist_nonneg.trans_lt hw
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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)
⊢ 0 ≤ R

Tactic:
hR.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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)
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
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w

Tactic:
lift R to ℝ≥0 using hR.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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)
⊢ 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
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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

Tactic:
this.continuousOn.continuousAt (Metric.isOpen_eball.mem_nhds ?_)

Premises used: Metric.isOpen_eball, IsOpen.mem_nhds, HasFPowerSeriesOnBall.continuousOn, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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∞)
refine : w ∈ eball 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

Tactic:
refine this.continuousOn.continuousAt (Metric.isOpen_eball.mem_nhds ?_)

Premises used: Metric.isOpen_eball, IsOpen.mem_nhds, HasFPowerSeriesOnBall.continuousOn, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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∞)
rwa rwa₁ rwa₂ rwa₃ : w ∈ ball c (↑R : ℝ)
⊢ w ∈ eball c (↑R : ℝ≥0∞)

Tactic:
rwa [Metric.eball_coe]

Premises used: Metric.eball_coe
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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

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]
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ ContinuousAt f w

Tactic:
have B : ContinuousAt f w := hc.continuousAt (closedBall_mem_nhds_of_mem hw)
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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

Tactic:
tendsto_nhds_unique_of_frequently_eq A B ((mem_closure_iff_frequently.1 this).mono ?_)

Premises used: mem_closure_iff_frequently, Filter.Frequently.mono, Iff.mp, tendsto_nhds_unique_of_frequently_eq
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
refine :
  ∀ x ∈ ball c (↑R : ℝ) \ s,
    HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - x)⁻¹ • f z) = f x
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - w)⁻¹ • f z) = f w

Tactic:
refine tendsto_nhds_unique_of_frequently_eq A B ((mem_closure_iff_frequently.1 this).mono ?_)

Premises used: mem_closure_iff_frequently, Filter.Frequently.mono, Iff.mp, tendsto_nhds_unique_of_frequently_eq
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
ha : 2 * (↑π : ℂ) * I ≠ 0
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z_1 : ℂ) in C(c, (↑R : ℝ)), (z_1 - z)⁻¹ • f z_1) = f z

Tactic:
rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux hs hz hc hd,
      inv_smul_smul₀]

Premises used: inv_smul_smul₀, Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ 2 * (↑π : ℂ) * I ≠ 0

Tactic:
simp [Real.pi_ne_zero, I_ne_zero]

Premises used: Complex.I_ne_zero, Real.pi_ne_zero