awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
suffices : w ∈ closure (ball c R \ s)
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w

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]
-- 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
⊢ w ∈ closure (ball c R \ s)

Tactic:
mem_closure_iff_nhds.2 fun t ht => ?_

Premises used: Iff.mpr, mem_closure_iff_nhds
-- 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
refine : ∀ (t : Set ℂ) (ht : t ∈ 𝓝 w), (t ∩ (ball c R \ s)).Nonempty
⊢ w ∈ closure (ball c R \ s)

Tactic:
refine mem_closure_iff_nhds.2 fun t ht => ?_

Premises used: Iff.mpr, mem_closure_iff_nhds
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
⊢ Continuous g

Tactic:
fun_prop
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
⊢ Tendsto g (𝓝 0) (𝓝 w)

Tactic:
have : Tendsto g (𝓝 0) (𝓝 w) := Continuous.tendsto' (by fun_prop) 0 w (add_zero _)
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this : Tendsto g (𝓝 0) (𝓝 w)
rcases : ∀ (l u : ℝ) (hlu₀ : 0 ∈ Ioo l u) (hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)), (t ∩ (ball c R \ s)).Nonempty
⊢ (t ∩ (ball c R \ s)).Nonempty

Tactic:
rcases mem_nhds_iff_exists_Ioo_subset.1 (this <| inter_mem ht <| isOpen_ball.mem_nhds hw) with
    ⟨l, u, hlu₀, hlu_sub⟩

Premises used: Filter.inter_mem, Metric.isOpen_ball, IsOpen.mem_nhds, Iff.mp, mem_nhds_iff_exists_Ioo_subset
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
⊢ (Ioo l u \ g ⁻¹' s).Nonempty

Tactic:
diff_nonempty.2 fun hsub => ?_

Premises used: Iff.mpr, Set.diff_nonempty
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
refine : ∀ (hsub : Ioo l u ⊆ g ⁻¹' s), False
⊢ (Ioo l u \ g ⁻¹' s).Nonempty

Tactic:
refine diff_nonempty.2 fun hsub => ?_

Premises used: Iff.mpr, Set.diff_nonempty
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
hsub : Ioo l u ⊆ g ⁻¹' s
⊢ (Ioo l u).Countable

Tactic:
have : (Ioo l u).Countable :=
      (hs.preimage ((add_right_injective w).comp ofReal_injective)).mono hsub
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this_1 : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
hsub : Ioo l u ⊆ g ⁻¹' s
this : (Ioo l u).Countable
⊢ Cardinal.continuum ≤ Cardinal.aleph0

Tactic:
rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this

Premises used: Cardinal.le_aleph0_iff_set_countable, And.right, And.left, LT.lt.trans, Cardinal.mk_Ioo_real
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this_1 : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
hsub : Ioo l u ⊆ g ⁻¹' s
this : Cardinal.continuum ≤ Cardinal.aleph0
⊢ False

Tactic:
this.not_gt Cardinal.aleph0_lt_continuum

Premises used: LE.le.not_gt, Cardinal.aleph0_lt_continuum
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this_1 : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
hsub : Ioo l u ⊆ g ⁻¹' s
this : Cardinal.continuum ≤ Cardinal.aleph0
⊢ False

Tactic:
exact this.not_gt Cardinal.aleph0_lt_continuum

Premises used: LE.le.not_gt, Cardinal.aleph0_lt_continuum
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
obtain : ∀ (x : ℝ) (hx : x ∈ Ioo l u \ g ⁻¹' s), (t ∩ (ball c R \ s)).Nonempty
⊢ (t ∩ (ball c R \ s)).Nonempty

Tactic:
obtain ⟨x, hx⟩ : (Ioo l u \ g ⁻¹' s).Nonempty := by
    refine diff_nonempty.2 fun hsub => ?_
    have : (Ioo l u).Countable :=
      (hs.preimage ((add_right_injective w).comp ofReal_injective)).mono hsub
    rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this
    exact this.not_gt Cardinal.aleph0_lt_continuum

Premises used: SDiff.sdiff, Set.Nonempty, Set.preimage, Set.Ioo
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
x : ℝ
hx : x ∈ Ioo l u \ g ⁻¹' s
⊢ (t ∩ (ball c R \ s)).Nonempty

Tactic:
⟨g x, (hlu_sub hx.1).1, (hlu_sub hx.1).2, hx.2⟩

Premises used: Set.Nonempty, And.right, And.left, And.intro, Exists.intro
-- 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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
x : ℝ
hx : x ∈ Ioo l u \ g ⁻¹' s
⊢ (t ∩ (ball c R \ s)).Nonempty

Tactic:
exact ⟨g x, (hlu_sub hx.1).1, (hlu_sub hx.1).2, hx.2⟩
-- 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
ha : 2 * (↑π : ℂ) * I ≠ 0
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w

Tactic:
rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
    hs hw hc hd, smul_inv_smul₀]

Premises used: smul_inv_smul₀, Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
-- 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
⊢ 2 * (↑π : ℂ) * I ≠ 0

Tactic:
simp [Real.pi_ne_zero, I_ne_zero]

Premises used: Complex.I_ne_zero, Real.pi_ne_zero
-- 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
h : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w

Tactic:
circleIntegral_sub_inv_smul_of_differentiable_on_off_countable countable_empty hw
    h.continuousOn_ball fun _x hx => h.differentiableAt isOpen_ball hx.1

Premises used: DiffContOnCl.continuousOn_ball, Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable, Metric.isOpen_ball, And.left, DiffContOnCl.differentiableAt, 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
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
⊢ 0 < R

Tactic:
have hR : 0 < R := not_le.mp (ball_eq_empty.not.mp (Set.nonempty_of_mem hw).ne_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
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w

Tactic:
two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
    countable_empty hw ?_ ?_

Premises used: Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_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
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
refine_1 : ContinuousOn f (closedBall c R)
refine_2 : ∀ x ∈ ball c R \ ∅, DifferentiableAt ℂ f x
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w

Tactic:
refine two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
    countable_empty hw ?_ ?_

Premises used: Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_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
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ContinuousOn f (closedBall c R)

Tactic:
simpa only [closure_ball c hR.ne.symm] using hf.continuousOn

Premises used: Ne.symm, DiffContOnCl.continuousOn, closure_ball, LT.lt.ne
-- 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
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ x ∈ ball c R \ ∅, DifferentiableAt ℂ f x

Tactic:
simpa only [diff_empty] using fun z hz => hf.differentiableAt isOpen_ball hz

Premises used: Set.diff_empty, Metric.isOpen_ball, DiffContOnCl.differentiableAt
-- 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
hd : DifferentiableOn ℂ f (closedBall c R)
hw : w ∈ ball c R
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w

Tactic:
(hd.mono closure_ball_subset_closedBall).diffContOnCl.circleIntegral_sub_inv_smul hw

Premises used: DiffContOnCl.circleIntegral_sub_inv_smul, Metric.closure_ball_subset_closedBall, DifferentiableOn.diffContOnCl, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
f : ℂ → ℂ
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, R), f z / (z - w) = 2 * (↑π : ℂ) * I * f w

Tactic:
simpa only [smul_eq_mul, div_eq_inv_mul] using
    circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd

Premises used: Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable, smul_eq_mul, div_eq_inv_mul
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ z ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : Membership.mem (γ := Set ℂ) (eball 0 (↑R : ℝ≥0∞)) w
⊢ c + w ∈ ball c (↑R : ℝ)

Tactic:
simpa only [add_mem_ball_iff_norm, ← coe_nnnorm, mem_eball_zero_iff,
        NNReal.coe_lt_coe, enorm_lt_coe] using hw

Premises used: add_mem_ball_iff_norm, enorm_lt_coe, coe_nnnorm, NNReal.coe_lt_coe, mem_eball_zero_iff
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ z ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : Membership.mem (γ := Set ℂ) (eball 0 (↑R : ℝ≥0∞)) w
⊢ c + w ∈ ball c (↑R : ℝ)

Tactic:
have hw' : c + w ∈ ball c R := by
      simpa only [add_mem_ball_iff_norm, ← coe_nnnorm, mem_eball_zero_iff,
        NNReal.coe_lt_coe, enorm_lt_coe] using hw
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ z ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : Membership.mem (γ := Set ℂ) (eball 0 (↑R : ℝ≥0∞)) w
hw' : c + w ∈ ball c (↑R : ℝ)
rw :
  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))
⊢ HasSum (fun (n : ℕ) ↦ (cauchyPowerSeries f c (↑R : ℝ) n : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ w) (f (c + w))

Tactic:
rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
      hs hw' hc hd]

Premises used: Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ z ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : Membership.mem (γ := Set ℂ) (eball 0 (↑R : ℝ≥0∞)) w
hw' : c + w ∈ ball c (↑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))

Tactic:
(hasFPowerSeriesOn_cauchy_integral
      ((hc.mono sphere_subset_closedBall).circleIntegrable R.2) hR).hasSum hw

Premises used: ContinuousOn.circleIntegrable, HasFPowerSeriesOnBall.hasSum, hasFPowerSeriesOn_cauchy_integral, ContinuousOn.mono, Metric.sphere_subset_closedBall, Subtype.property
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ z ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : Membership.mem (γ := Set ℂ) (eball 0 (↑R : ℝ≥0∞)) w
hw' : c + w ∈ ball c (↑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))

Tactic:
exact (hasFPowerSeriesOn_cauchy_integral
      ((hc.mono sphere_subset_closedBall).circleIntegrable R.2) hR).hasSum hw

Premises used: ContinuousOn.circleIntegrable, HasFPowerSeriesOnBall.hasSum, hasFPowerSeriesOn_cauchy_integral, ContinuousOn.mono, Metric.sphere_subset_closedBall, Subtype.property
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c (↑R : ℝ))
hR : 0 < R
⊢ HasFPowerSeriesOnBall f (cauchyPowerSeries f c (↑R : ℝ)) c (↑R : ℝ≥0∞)

Tactic:
hasFPowerSeriesOnBall_of_differentiable_off_countable countable_empty hf.continuousOn_ball
    (fun _z hz => hf.differentiableAt isOpen_ball hz.1) hR

Premises used: DiffContOnCl.continuousOn_ball, Metric.isOpen_ball, And.left, DiffContOnCl.differentiableAt, Complex.hasFPowerSeriesOnBall_of_differentiable_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 : ℝ≥0
c : ℂ
f : ℂ → E
hd : DifferentiableOn ℂ f (closedBall c (↑R : ℝ))
hR : 0 < R
⊢ HasFPowerSeriesOnBall f (cauchyPowerSeries f c (↑R : ℝ)) c (↑R : ℝ≥0∞)

Tactic:
(hd.mono closure_ball_subset_closedBall).diffContOnCl.hasFPowerSeriesOnBall hR

Premises used: Metric.closure_ball_subset_closedBall, DifferentiableOn.diffContOnCl, DifferentiableOn.mono, DiffContOnCl.hasFPowerSeriesOnBall
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
rcases : ∀ (R : ℝ) (hR0 : 0 < R) (hRs : closedBall z R ⊆ s), AnalyticAt ℂ f z
⊢ AnalyticAt ℂ f z

Tactic:
rcases nhds_basis_closedBall.mem_iff.1 hz with ⟨R, hR0, hRs⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
R : ℝ
hR0 : 0 < R
hRs : closedBall z R ⊆ s
⊢ 0 ≤ R

Tactic:
hR0.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
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
R : ℝ
hR0 : 0 < R
hRs : closedBall z R ⊆ s
lift : ∀ (R : ℝ≥0) (hR0 : 0 < (↑R : ℝ)) (hRs : closedBall z (↑R : ℝ) ⊆ s), AnalyticAt ℂ f z
⊢ AnalyticAt ℂ f z

Tactic:
lift R to ℝ≥0 using hR0.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
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall z (↑R : ℝ) ⊆ s
⊢ AnalyticAt ℂ f z

Tactic:
((hd.mono hRs).hasFPowerSeriesOnBall hR0).analyticAt

Premises used: DifferentiableOn.hasFPowerSeriesOnBall, HasFPowerSeriesOnBall.analyticAt, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall z (↑R : ℝ) ⊆ s
⊢ AnalyticAt ℂ f z

Tactic:
exact ((hd.mono hRs).hasFPowerSeriesOnBall hR0).analyticAt

Premises used: DifferentiableOn.hasFPowerSeriesOnBall, HasFPowerSeriesOnBall.analyticAt, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
s : Set ℂ
f : ℂ → E
hd : DifferentiableOn ℂ f s
hs : IsOpen s
⊢ AnalyticOnNhd ℂ f s

Tactic:
fun _z hz => hd.analyticAt (hs.mem_nhds hz)

Premises used: AnalyticOnNhd, IsOpen.mem_nhds, DifferentiableOn.analyticAt
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
s : Set ℂ
f : ℂ → E
hd : DifferentiableOn ℂ f s
hs : IsOpen s
⊢ AnalyticOn ℂ f s

Tactic:
(hd.analyticOnNhd hs).analyticOn

Premises used: AnalyticOnNhd.analyticOn, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
s : Set ℂ
f : ℂ → E
n : WithTop ℕ∞
hd : DifferentiableOn ℂ f s
hs : IsOpen s
⊢ ContDiffOn ℂ n f s

Tactic:
(hd.analyticOnNhd hs).contDiffOn_of_completeSpace

Premises used: AnalyticOnNhd.contDiffOn_of_completeSpace, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
s : Set ℂ
f : ℂ → E
hd : DifferentiableOn ℂ f s
hs : IsOpen s
⊢ DifferentiableOn ℂ (deriv f) s

Tactic:
(hd.analyticOnNhd hs).deriv.differentiableOn

Premises used: AnalyticOnNhd.deriv, DifferentiableOn.analyticOnNhd, AnalyticOnNhd.differentiableOn
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
hf : Differentiable ℂ f
z : ℂ
⊢ AnalyticAt ℂ f z

Tactic:
hf.differentiableOn.analyticAt univ_mem

Premises used: Differentiable.differentiableOn, DifferentiableOn.analyticAt, Filter.univ_mem