awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r R : ℝ
h0 : 0 < r
hle : r ≤ R
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ ball c r)
hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z
⊢ let A := closedBall c R \ ball c r;
  ContinuousOn f A

Tactic:
set A := closedBall c R \ ball c r

Premises used: Metric.ball, Metric.closedBall
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r R : ℝ
h0 : 0 < r
hle : r ≤ R
f : ℂ → E
s : Set ℂ
hs : s.Countable
hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c R \ ball c r
hc : ContinuousOn f A
⊢ ∃ (a : ℝ), rexp a = r

Tactic:
⟨Real.log r, Real.exp_log h0⟩

Premises used: Real.exp_log, Real.log, Exists.intro
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r R : ℝ
h0 : 0 < r
hle : r ≤ R
f : ℂ → E
s : Set ℂ
hs : s.Countable
hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c R \ ball c r
hc : ContinuousOn f A
obtain :
  ∀ (a : ℝ) (h0 : 0 < rexp a) (hle : rexp a ≤ R)
    (hd : ∀ z ∈ (ball c R \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z),
    let A := closedBall c R \ ball c (rexp a);
    ∀ (hc : ContinuousOn f A),
      Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z)
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z)

Tactic:
obtain ⟨a, rfl⟩ : ∃ a, Real.exp a = r := ⟨Real.log r, Real.exp_log h0⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
hle : rexp a ≤ R
hd : ∀ z ∈ (ball c R \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c R \ ball c (rexp a)
hc : ContinuousOn f A
⊢ ∃ (b : ℝ), rexp b = R

Tactic:
⟨Real.log R, Real.exp_log (h0.trans_le hle)⟩

Premises used: Real.exp_log, Real.log, LT.lt.trans_le, Exists.intro
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
hle : rexp a ≤ R
hd : ∀ z ∈ (ball c R \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c R \ ball c (rexp a)
hc : ContinuousOn f A
obtain :
  ∀ (b : ℝ) (hle : rexp a ≤ rexp b) (hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z),
    let A := closedBall c (rexp b) \ ball c (rexp a);
    ∀ (hc : ContinuousOn f A),
      Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z)
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z)

Tactic:
obtain ⟨b, rfl⟩ : ∃ b, Real.exp b = R := ⟨Real.log R, Real.exp_log (h0.trans_le hle)⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : rexp a ≤ rexp b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
⊢ a ≤ b

Tactic:
rw [Real.exp_le_exp] at hle

Premises used: Real.exp_le_exp
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : rexp a ≤ rexp b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
hle₁ : a ≤ b
⊢ ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z

Tactic:
rw [Real.exp_le_exp] at hle

Premises used: Real.exp_le_exp
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : rexp a ≤ rexp b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
hle₁ : a ≤ b
hd₁ : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
⊢ let A := closedBall c (rexp b) \ ball c (rexp a);
  ContinuousOn f A

Tactic:
rw [Real.exp_le_exp] at hle

Premises used: Real.exp_le_exp
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
this :
  Eq.{u + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ))
    (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ))
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z)

Tactic:
simpa only [circleIntegral, add_sub_cancel_left, ofReal_exp, ← exp_add, smul_smul, ←
      div_eq_mul_inv, mul_div_cancel_left₀ _ (circleMap_ne_center (Real.exp_pos _).ne'),
      circleMap_sub_center, deriv_circleMap]

Premises used: Complex.exp_add, circleMap_sub_center, add_sub_cancel_left, smul_smul, mul_div_cancel_left₀, Complex.ofReal_exp, circleMap_ne_center, div_eq_mul_inv, LT.lt.ne', deriv_circleMap, circleIntegral, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
θ :
  Eq.{u + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ))
    (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ))
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z)

Tactic:
suffices
    (∫ θ in 0..2 * π, I • f (circleMap c (Real.exp b) θ)) =
      ∫ θ in 0..2 * π, I • f (circleMap c (Real.exp a) θ) by
    simpa only [circleIntegral, add_sub_cancel_left, ofReal_exp, ← exp_add, smul_smul, ←
      div_eq_mul_inv, mul_div_cancel_left₀ _ (circleMap_ne_center (Real.exp_pos _).ne'),
      circleMap_sub_center, deriv_circleMap]
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
⊢ Differentiable ℂ g

Tactic:
have hdg : Differentiable ℂ g := differentiable_exp.const_add _
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
⊢ (g ⁻¹' s).Countable

Tactic:
replace hs : (g ⁻¹' s).Countable := (hs.preimage (add_right_injective c)).preimage_cexp
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
z : ℂ
h : z ∈ re ⁻¹' [[a, b]]
⊢ g z ∈ A

Tactic:
simpa [g, A, dist_eq, norm_exp, hle] using h.symm

Premises used: Complex.dist_eq, Complex.norm_exp, And.symm
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
⊢ MapsTo g R A

Tactic:
have h_maps : MapsTo g R A := by
    rintro z ⟨h, -⟩; simpa [g, A, dist_eq, norm_exp, hle] using h.symm
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
⊢ ContinuousOn (f ∘ g) R

Tactic:
replace hc : ContinuousOn (f ∘ g) R := hc.comp hdg.continuous.continuousOn h_maps
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
⊢ ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z

Tactic:
fun z hz => (hd (g z) ⟨?_, hz.2⟩).comp z (hdg _)

Premises used: And.right, And.intro, DifferentiableAt.comp
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
refine :
  ∀ (z : ℂ) (hz : z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s),
    g z ∈ ball c (rexp b) \ closedBall c (rexp a)
⊢ ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z

Tactic:
refine fun z hz => (hd (g z) ⟨?_, hz.2⟩).comp z (hdg _)

Premises used: And.intro, DifferentiableAt.comp
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
z : ℂ
hz : z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s
⊢ g z ∈ ball c (rexp b) \ closedBall c (rexp a)

Tactic:
simpa [g, dist_eq, norm_exp, hle, and_comm] using hz.1.1

Premises used: and_comm, Complex.dist_eq, And.left, Complex.norm_exp
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
⊢ ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z

Tactic:
replace hd : ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s,
      DifferentiableAt ℂ (f ∘ g) z := by
    refine fun z hz => (hd (g z) ⟨?_, hz.2⟩).comp z (hdg _)
    simpa [g, dist_eq, norm_exp, hle, and_comm] using hz.1.1
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
hd : ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z
⊢ Eq.{u + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ))
    (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ))

Tactic:
simpa [g, circleMap, exp_periodic _, sub_eq_zero, ← exp_add] using
    integral_boundary_rect_eq_zero_of_differentiable_on_off_countable _ ⟨a, 0⟩ ⟨b, 2 * π⟩ _ hs hc hd

Premises used: Real.pi, HMul.hMul, Complex.exp_add, sub_eq_zero, Complex.exp_periodic, circleMap, Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable, OfNat.ofNat, Complex.mk
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r R : ℝ
h0 : 0 < r
hle : r ≤ R
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ ball c r)
hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) (∮ (z : ℂ) in C(c, r), f z)

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
    _ = ∮ z in C(c, r), (z - c)⁻¹ • (z - c) • f z :=
      (circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable h0 hle hs
        ((continuousOn_id.sub continuousOn_const).smul hc) fun z hz =>
        (differentiableAt_id.sub_const _).smul (hd z hz))
    _ = ∮ z in C(c, r), f z := circleIntegral.integral_sub_inv_smul_sub_smul _ _ _ _

Premises used: Trans.trans, circleIntegral.integral_sub_inv_smul_sub_smul, DifferentiableAt.smul, ContinuousOn.sub, continuousOn_const, Complex.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable, ContinuousOn.smul, continuousOn_id, Eq.symm
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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)
rw : ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ 0
⊢ ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z = (2 * (↑π : ℂ) * I) • y

Tactic:
rw [← sub_eq_zero, ← norm_le_zero_iff]

Premises used: sub_eq_zero, norm_le_zero_iff
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ 0

Tactic:
le_of_forall_gt_imp_ge_of_dense fun ε ε0 => ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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)
refine : ∀ (ε : ℝ) (ε0 : 0 < ε), ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ ε
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ 0

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun ε ε0 => ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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, ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)

Tactic:
((nhdsWithin_hasBasis nhds_basis_closedBall _).tendsto_iff nhds_basis_ball).1 hy _
      (div_pos ε0 Real.two_pi_pos)

Premises used: Filter.HasBasis.tendsto_iff, Set.Mem, Set.diff, setOf, Metric.ball, Real.two_pi_pos, Iff.mp, nhdsWithin_hasBasis, div_pos, Metric.nhds_basis_ball, Metric.nhds_basis_closedBall, Not
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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 < ε
obtain :
  ∀ (δ : ℝ) (δ0 : δ > 0) (hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)),
    ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ ε
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ ε

Tactic:
obtain ⟨δ, δ0, hδ⟩ : ∃ δ > (0 : ℝ), ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π) :=
    ((nhdsWithin_hasBasis nhds_basis_closedBall _).tendsto_iff nhds_basis_ball).1 hy _
      (div_pos ε0 Real.two_pi_pos)

Premises used: Real.pi, HMul.hMul, Filter.HasBasis.tendsto_iff, Real.two_pi_pos, Iff.mp, nhdsWithin_hasBasis, div_pos, Metric.nhds_basis_ball, Metric.nhds_basis_closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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 : ℝ), 0 < r ∧ r ≤ δ ∧ r ≤ R

Tactic:
⟨min δ R, lt_min δ0 h0, min_le_left _ _, min_le_right _ _⟩

Premises used: lt_min, min_le_left, And.intro, min_le_right, Exists.intro, Min.min
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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 * π)
obtain :
  ∀ (r : ℝ) (hr0 : 0 < r) (hrδ : r ≤ δ) (hrR : r ≤ R),
    ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ ε
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ ε

Tactic:
obtain ⟨r, hr0, hrδ, hrR⟩ : ∃ r, 0 < r ∧ r ≤ δ ∧ r ≤ R :=
    ⟨min δ R, lt_min δ0 h0, min_le_left _ _, min_le_right _ _⟩
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ closedBall c R \ ball c r ⊆ closedBall c R \ {c}

Tactic:
have hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c} :=
    diff_subset_diff_right (singleton_subset_iff.2 <| mem_ball_self hr0)
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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}
⊢ ball c R \ closedBall c r ⊆ ball c R \ {c}

Tactic:
have hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c} :=
    diff_subset_diff_right (singleton_subset_iff.2 <| mem_closedBall_self hr0.le)
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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}
⊢ ∀ z ∈ sphere c r, z ≠ c

Tactic:
have hzne : ∀ z ∈ sphere c r, z ≠ c := fun z hz =>
    ne_of_mem_of_not_mem hz fun h => hr0.ne' <| dist_self c ▸ Eq.symm h
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
e_a : Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z)
e_a₁ : (2 * (↑π : ℂ) * I) • y = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y
⊢ ‖(∮ (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)‖

Tactic:
congr 2
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z)

Tactic:
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⟩

Premises used: Complex.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable, And.right, And.left, And.intro, ContinuousOn.mono