awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun (θ' : ℝ) ↦ circleMap c R θ' - circleMap c R θ
this_1 : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
θ' : ℝ
hθ' : Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
x : ℝ := ‖f θ'‖
this : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ n < HAdd.hAdd (α := ℤ) (-1) 1

Tactic:
hn

Premises used: Int.subNatNat, Int.add
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun (θ' : ℝ) ↦ circleMap c R θ' - circleMap c R θ
this_1 : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
θ' : ℝ
hθ' : Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
x : ℝ := ‖f θ'‖
this : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ n < HAdd.hAdd (α := ℤ) (-1) 1

Tactic:
exact hn
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
n : ℤ
⊢ CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c 0

Tactic:
circleIntegrable_zero_radius

Premises used: circleIntegrable_zero_radius
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
n : ℤ
H : 0 ≤ n ∨ w ∉ sphere c |R|
⊢ CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R

Tactic:
((continuousOn_id.sub continuousOn_const).zpow₀ _ fun z hz =>
        H.symm.imp_left fun (hw : w ∉ sphere c |R|) =>
          sub_ne_zero.2 <| ne_of_mem_of_not_mem hz hw).circleIntegrable'

Premises used: Iff.mpr, Or.imp_left, sub_ne_zero, ContinuousOn.sub, continuousOn_const, ne_of_mem_of_not_mem, Or.symm, ContinuousOn.zpow₀, ContinuousOn.circleIntegrable', continuousOn_id
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
n : ℤ
⊢ CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c 0

Tactic:
exacts [circleIntegrable_zero_radius,
      ((continuousOn_id.sub continuousOn_const).zpow₀ _ fun z hz =>
        H.symm.imp_left fun (hw : w ∉ sphere c |R|) =>
          sub_ne_zero.2 <| ne_of_mem_of_not_mem hz hw).circleIntegrable']

Premises used: circleIntegrable_zero_radius
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
simp : R = 0 ∨ LE.le (α := ℤ) 0 (-1) ∨ w ∉ sphere c |R| ↔ R = 0 ∨ w ∉ sphere c |R|
⊢ CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w)⁻¹) c R ↔ R = 0 ∨ w ∉ sphere c |R|

Tactic:
simp only [← zpow_neg_one, circleIntegrable_sub_zpow_iff]

Premises used: zpow_neg_one, circleIntegrable_sub_zpow_iff
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
⊢ R = 0 ∨ LE.le (α := ℤ) 0 (-1) ∨ w ∉ sphere c |R| ↔ R = 0 ∨ w ∉ sphere c |R|

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
rw :
  Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, deriv (circleMap c R) θ • f (circleMap c R θ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (θ : ℝ) ↦
      deriv (circleMap c R) θ • f (circleMap c R θ))
rw₁ :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (2 * π))) fun (x : ℝ) ↦
      deriv (circleMap c R) x • f (circleMap c R x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (θ : ℝ) ↦
      deriv (circleMap c R) θ • f (circleMap c R θ))
rw₂ rw₃ :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (x : ℝ) ↦
      deriv (circleMap c R) x • f (circleMap c R x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (θ : ℝ) ↦
      deriv (circleMap c R) θ • f (circleMap c R θ))
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (θ : ℝ) ↦
      deriv (circleMap c R) θ • f (circleMap c R θ))

Tactic:
rw [circleIntegral, intervalIntegral.integral_of_le Real.two_pi_pos.le,
    Measure.restrict_congr_set Ioc_ae_eq_Icc]

Premises used: MeasureTheory.Measure.restrict_congr_set, LT.lt.le, MeasureTheory.Ioc_ae_eq_Icc, Real.two_pi_pos, intervalIntegral.integral_of_le, circleIntegral
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
hF :
  ∀ᶠ (i : ι) in l,
    ContinuousOn.{0, u_1} (Y := E)
      (fun (x : ℝ) ↦ HSMul.hSMul (β := E) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f i z) (circleMap c R x)))
      [[0, 2 * π]]
h_lim :
  TendstoUniformlyOn.{0, u_1, u_2} (β := E)
    (fun (n : ι) (x : ℝ) ↦ HSMul.hSMul (β := E) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f n z) (circleMap c R x)))
    (fun (x : ℝ) ↦ HSMul.hSMul (β := E) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ g z) (circleMap c R x))) l
    [[0, 2 * π]]
⊢ Tendsto.{u_2, u_1} (β := E) (fun (n : ι) ↦ ∮ (z : ℂ) in C(c, R), f n z) l (𝓝 (∮ (z : ℂ) in C(c, R), g z))

Tactic:
apply TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn

Premises used: TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
⊢ ∀ᶠ (i : ι) in l,
    ContinuousOn.{0, u_1} (Y := E)
      (fun (x : ℝ) ↦ HSMul.hSMul (β := E) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f i z) (circleMap c R x)))
      [[0, 2 * π]]

Tactic:
hf.mono fun i hi ↦ .smul ?_ (hi.comp ?_ ?_)

Premises used: Filter.Eventually.mono, ContinuousOn.comp, ContinuousOn.smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
hF : ∀ (i : ι) (hi : ContinuousOn (f i) (sphere c R)), ContinuousOn (deriv (circleMap c R)) [[0, 2 * π]]
hF₁ : ∀ (i : ι) (hi : ContinuousOn (f i) (sphere c R)), ContinuousOn (circleMap c R) [[0, 2 * π]]
hF₂ : ∀ (i : ι) (hi : ContinuousOn (f i) (sphere c R)), MapsTo (circleMap c R) [[0, 2 * π]] (sphere c R)
⊢ ∀ᶠ (i : ι) in l,
    ContinuousOn.{0, u_1} (Y := E)
      (fun (x : ℝ) ↦ HSMul.hSMul (β := E) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f i z) (circleMap c R x)))
      [[0, 2 * π]]

Tactic:
refine hf.mono fun i hi ↦ .smul ?_ (hi.comp ?_ ?_)

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
hF : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ circleMap 0 R x * I) [[0, 2 * π]]
⊢ ContinuousOn (deriv (circleMap c R)) [[0, 2 * π]]

Tactic:
rw [funext (deriv_circleMap _ _)]

Premises used: deriv_circleMap, funext
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ circleMap 0 R x * I) [[0, 2 * π]]

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ ContinuousOn (circleMap c R) [[0, 2 * π]]

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ MapsTo (circleMap c R) [[0, 2 * π]] (sphere c R)

Tactic:
simp [hR, MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
h_lim :
  ∀ (h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε),
    ∀ ε > 0,
      ∀ᶠ (n : ι) in l,
        ∀ x ∈ [[0, 2 * π]],
          dist (HSMul.hSMul (β := E) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ g z) (circleMap c R x)))
              (HSMul.hSMul (β := E) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f n z) (circleMap c R x))) <
            ε
⊢ TendstoUniformlyOn.{0, u_1, u_2} (β := E)
    (fun (n : ι) (x : ℝ) ↦ HSMul.hSMul (β := E) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f n z) (circleMap c R x)))
    (fun (x : ℝ) ↦ HSMul.hSMul (β := E) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ g z) (circleMap c R x))) l
    [[0, 2 * π]]

Tactic:
rw [Metric.tendstoUniformlyOn_iff] at h ⊢

Premises used: Metric.tendstoUniformlyOn_iff
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
h_lim : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ [[0, 2 * π]], R * dist (g (circleMap c R x)) (f n (circleMap c R x)) < ε
⊢ ∀ ε > 0,
    ∀ᶠ (n : ι) in l,
      ∀ x ∈ [[0, 2 * π]],
        dist (HSMul.hSMul (β := E) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ g z) (circleMap c R x)))
            (HSMul.hSMul (β := E) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f n z) (circleMap c R x))) <
          ε

Tactic:
simp only [dist_smul₀, deriv_circleMap, norm_mul, norm_I, norm_circleMap_zero,
      abs_of_nonneg hR, mul_one]

Premises used: norm_circleMap_zero, norm_mul, deriv_circleMap, Complex.norm_I, abs_of_nonneg, dist_smul₀, mul_one
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
h_lim :
  ∀ (δ : ℝ) (hδ₀ : 0 < δ) (hRδ : R * δ < ε),
    ∀ᶠ (n : ι) in l, ∀ x ∈ [[0, 2 * π]], R * dist (g (circleMap c R x)) (f n (circleMap c R x)) < ε
⊢ ∀ᶠ (n : ι) in l, ∀ x ∈ [[0, 2 * π]], R * dist (g (circleMap c R x)) (f n (circleMap c R x)) < ε

Tactic:
rcases exists_pos_mul_lt hε R with ⟨δ, hδ₀, hRδ⟩

Premises used: exists_pos_mul_lt
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ₀ : 0 < δ
hRδ : R * δ < ε
⊢ ∀ᶠ (n : ι) in l, ∀ x ∈ [[0, 2 * π]], R * dist (g (circleMap c R x)) (f n (circleMap c R x)) < ε

Tactic:
(h δ hδ₀).mono fun i hi x hx ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ₀ : 0 < δ
hRδ : R * δ < ε
h_lim :
  ∀ (i : ι) (hi : ∀ x ∈ sphere c R, dist (g x) (f i x) < δ) (x : ℝ) (hx : x ∈ [[0, 2 * π]]),
    R * dist (g (circleMap c R x)) (f i (circleMap c R x)) < ε
⊢ ∀ᶠ (n : ι) in l, ∀ x ∈ [[0, 2 * π]], R * dist (g (circleMap c R x)) (f n (circleMap c R x)) < ε

Tactic:
refine (h δ hδ₀).mono fun i hi x hx ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ₀ : 0 < δ
hRδ : R * δ < ε
i : ι
hi : ∀ x ∈ sphere c R, dist (g x) (f i x) < δ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ circleMap c R x ∈ sphere c R

Tactic:
simp [hR]
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ₀ : 0 < δ
hRδ : R * δ < ε
i : ι
hi : ∀ x ∈ sphere c R, dist (g x) (f i x) < δ
x : ℝ
hx : x ∈ [[0, 2 * π]]
h_lim : R * δ < ε
⊢ R * dist (g (circleMap c R x)) (f i (circleMap c R x)) < ε

Tactic:
grw [hi (circleMap c R x) (by simp [hR])]

Premises used: circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ₀ : 0 < δ
hRδ : R * δ < ε
i : ι
hi : ∀ x ∈ sphere c R, dist (g x) (f i x) < δ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ R * δ < ε

Tactic:
hRδ
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ₀ : 0 < δ
hRδ : R * δ < ε
i : ι
hi : ∀ x ∈ sphere c R, dist (g x) (f i x) < δ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ R * δ < ε

Tactic:
exact hRδ
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, 0), f z) 0

Tactic:
simp +unfoldPartialApp [circleIntegral, const]

Premises used: Function.const, circleIntegral
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
c : ℂ
R : ℝ
hR : 0 ≤ R
h : EqOn f g (sphere c R)
θ : ℝ
h_1 : θ ∈ [[0, 2 * π]]
⊢ HSMul.hSMul (β := E) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ f z) (circleMap c R θ)) =
    HSMul.hSMul (β := E) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ g z) (circleMap c R θ))

Tactic:
simp only [h (circleMap_mem_sphere _ hR _)]

Premises used: circleMap_mem_sphere
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
h :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ι 0 (2 * π)))).EventuallyEq (β := ℂ)
    (fun (x : ℝ) ↦ HSMul.hSMul (β := ℂ) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f₁ z) (circleMap c R x)))
    fun (x : ℝ) ↦ HSMul.hSMul (β := ℂ) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f₂ z) (circleMap c R x))
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), f₁ z) (∮ (z : ℂ) in C(c, R), f₂ z)

Tactic:
apply intervalIntegral.integral_congr_ae_restrict

Premises used: intervalIntegral.integral_congr_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
h :
  {x : ℝ |
      (fun (x : ℝ) ↦
          Eq (α := ℂ)
            ((fun (x : ℝ) ↦ HSMul.hSMul (β := ℂ) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f₁ z) (circleMap c R x))) x)
            ((fun (x : ℝ) ↦ HSMul.hSMul (β := ℂ) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f₂ z) (circleMap c R x))) x))
        x} ∈
    codiscreteWithin (Ι 0 (2 * π))
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ι 0 (2 * π)))).EventuallyEq (β := ℂ)
    (fun (x : ℝ) ↦ HSMul.hSMul (β := ℂ) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f₁ z) (circleMap c R x)))
    fun (x : ℝ) ↦ HSMul.hSMul (β := ℂ) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f₂ z) (circleMap c R x))

Tactic:
apply ae_restrict_le_codiscreteWithin measurableSet_uIoc

Premises used: measurableSet_uIoc, ae_restrict_le_codiscreteWithin
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
h : {x : ℝ | f₁ (circleMap c R x) = f₂ (circleMap c R x)} ∈ codiscreteWithin (Ι 0 (2 * π))
⊢ {x : ℝ |
      (fun (x : ℝ) ↦
          Eq (α := ℂ)
            ((fun (x : ℝ) ↦ HSMul.hSMul (β := ℂ) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f₁ z) (circleMap c R x))) x)
            ((fun (x : ℝ) ↦ HSMul.hSMul (β := ℂ) (deriv (circleMap c R) x) ((fun (z : ℂ) ↦ f₂ z) (circleMap c R x))) x))
        x} ∈
    codiscreteWithin (Ι 0 (2 * π))

Tactic:
simp only [deriv_circleMap, smul_eq_mul, mul_eq_mul_left_iff, mul_eq_zero,
    circleMap_eq_center_iff, hR, Complex.I_ne_zero, or_self, or_false]

Premises used: mul_eq_mul_left_iff, Complex.I_ne_zero, mul_eq_zero, deriv_circleMap, circleMap_eq_center_iff, or_self, or_false, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ ⦃a : ℝ⦄, a ∈ Ι 0 (2 * π) → Membership.mem (γ := Set ℝ) univ a
⊢ Ι 0 (2 * π) ⊆ univ

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ {x : ℝ | f₁ (circleMap c R x) = f₂ (circleMap c R x)} ∈ codiscreteWithin (Ι 0 (2 * π))

Tactic:
exact codiscreteWithin_mono (by tauto) (circleMap_preimage_codiscrete hR hf)

Premises used: Filter.codiscreteWithin_mono, circleMap_preimage_codiscrete
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
inl : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, 0), (z - w)⁻¹ • (z - w) • f z) (∮ (z : ℂ) in C(c, 0), f z)
inr :
  ∀ (hR : R ≠ 0), Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) (∮ (z : ℂ) in C(c, R), f z)
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) (∮ (z : ℂ) in C(c, R), f z)

Tactic:
rcases eq_or_ne R 0 with (rfl | hR)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, 0), (z - w)⁻¹ • (z - w) • f z) (∮ (z : ℂ) in C(c, 0), f z)

Tactic:
simp only [integral_radius_zero]

Premises used: circleIntegral.integral_radius_zero
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
⊢ (circleMap c R ⁻¹' {w}).Countable

Tactic:
have : (circleMap c R ⁻¹' {w}).Countable := (countable_singleton _).preimage_circleMap c hR
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) (∮ (z : ℂ) in C(c, R), f z)

Tactic:
intervalIntegral.integral_congr_ae ((this.ae_notMem _).mono fun θ hθ _' => ?_)

Premises used: Set.Countable.ae_notMem, Filter.Eventually.mono, circleIntegral, intervalIntegral.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
inr :
  ∀ (θ : ℝ) (hθ : θ ∉ circleMap c R ⁻¹' {w}) (_' : θ ∈ Ι 0 (2 * π)),
    HSMul.hSMul (β := E) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ (z - w)⁻¹ • (z - w) • f z) (circleMap c R θ)) =
      HSMul.hSMul (β := E) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ f z) (circleMap c R θ))
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) (∮ (z : ℂ) in C(c, R), f z)

Tactic:
refine intervalIntegral.integral_congr_ae ((this.ae_notMem _).mono fun θ hθ _' => ?_)

Premises used: Set.Countable.ae_notMem, Filter.Eventually.mono, intervalIntegral.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
θ : ℝ
hθ : θ ∉ circleMap c R ⁻¹' {w}
_' : θ ∈ Ι 0 (2 * π)
⊢ circleMap c R θ ≠ w

Tactic:
change circleMap c R θ ≠ w at hθ

Premises used: circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
θ : ℝ
_' : θ ∈ Ι 0 (2 * π)
hθ : circleMap c R θ ≠ w
⊢ HSMul.hSMul (β := E) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ (z - w)⁻¹ • (z - w) • f z) (circleMap c R θ)) =
    HSMul.hSMul (β := E) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ f z) (circleMap c R θ))

Tactic:
simp only [inv_smul_smul₀ (sub_ne_zero.2 <| hθ)]

Premises used: Iff.mpr, inv_smul_smul₀, sub_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
hf : ¬CircleIntegrable f c R
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f z) 0

Tactic:
intervalIntegral.integral_undef (mt (circleIntegrable_iff R).mpr hf)

Premises used: Iff.mpr, circleIntegrable_iff, mt, circleIntegral, intervalIntegral.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
c : ℂ
R : ℝ
hf : CircleIntegrable f c R
hg : CircleIntegrable g c R
⊢ ∮ (z : ℂ) in C(c, R), f z + g z = HAdd.hAdd (α := E) (∮ (z : ℂ) in C(c, R), f z) (∮ (z : ℂ) in C(c, R), g z)

Tactic:
simp only [circleIntegral, smul_add, intervalIntegral.integral_add hf.out hg.out]

Premises used: intervalIntegral.integral_add, circleIntegral, CircleIntegrable.out, smul_add
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
c : ℂ
R : ℝ
hf : CircleIntegrable f c R
hg : CircleIntegrable g c R
⊢ ∮ (z : ℂ) in C(c, R), f z - g z = HSub.hSub (α := E) (∮ (z : ℂ) in C(c, R), f z) (∮ (z : ℂ) in C(c, R), g z)

Tactic:
simp only [circleIntegral, smul_sub, intervalIntegral.integral_sub hf.out hg.out]

Premises used: intervalIntegral.integral_sub, smul_sub, circleIntegral, CircleIntegrable.out