awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : ¬R = 0
rw :
  ∃ s ∈ codiscreteWithin (Ι 0 (2 * π)),
    EqOn.{0, u_1} (β := E) (fun (θ : ℝ) ↦ f₁ (circleMap c R θ)) (fun (θ : ℝ) ↦ f₂ (circleMap c R θ)) s
⊢ EventuallyEq.{0, u_1} (β := E) (codiscreteWithin (Ι 0 (2 * π))) (fun (θ : ℝ) ↦ f₁ (circleMap c R θ)) fun (θ : ℝ) ↦
    f₂ (circleMap c R θ)

Tactic:
rw [eventuallyEq_iff_exists_mem]

Premises used: Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : ¬R = 0
⊢ Ι 0 (2 * π) ⊆ univ

Tactic:
simp only [Set.subset_univ]

Premises used: Set.subset_univ
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : ¬R = 0
tauto tauto₁ tauto₂ :
  ∀ ⦃x : ℝ⦄,
    x ∈ circleMap c R ⁻¹' {z : ℂ | f₁ z = f₂ z} →
      Eq.{u_1 + 1} (α := E) ((fun (θ : ℝ) ↦ f₁ (circleMap c R θ)) x) ((fun (θ : ℝ) ↦ f₂ (circleMap c R θ)) x)
⊢ EqOn.{0, u_1} (β := E) (fun (θ : ℝ) ↦ f₁ (circleMap c R θ)) (fun (θ : ℝ) ↦ f₂ (circleMap c R θ))
    (circleMap c R ⁻¹' {z : ℂ | f₁ z = f₂ z})

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : ¬R = 0
⊢ ∃ s ∈ codiscreteWithin (Ι 0 (2 * π)),
    EqOn.{0, u_1} (β := E) (fun (θ : ℝ) ↦ f₁ (circleMap c R θ)) (fun (θ : ℝ) ↦ f₂ (circleMap c R θ)) s

Tactic:
exact ⟨(circleMap c R)⁻¹' {z | f₁ z = f₂ z},
    codiscreteWithin_mono (by simp only [Set.subset_univ]) (circleMap_preimage_codiscrete hR hf),
    by tauto⟩
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
⊢ CircleIntegrable f₁ c R ↔ CircleIntegrable f₂ c R

Tactic:
⟨(CircleIntegrable.congr_codiscreteWithin hf ·),
    (CircleIntegrable.congr_codiscreteWithin hf.symm ·)⟩

Premises used: Iff.intro, CircleIntegrable.congr_codiscreteWithin, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
pos :
  ∀ (h₀ : R = 0),
    CircleIntegrable f c R ↔
      IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
neg :
  ∀ (h₀ : ¬R = 0),
    CircleIntegrable f c R ↔
      IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
⊢ CircleIntegrable f c R ↔
    IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
by_cases h₀ : R = 0
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : R = 0
⊢ CircleIntegrable f c R ↔
    IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
simp +unfoldPartialApp [h₀, const]

Premises used: Function.const
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
⊢ CircleIntegrable f c R ↔
    IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
⟨fun h => h.out, fun h => ?_⟩

Premises used: Iff.intro, CircleIntegrable.out
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
neg :
  ∀
    (h :
      IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)),
    CircleIntegrable f c R
⊢ CircleIntegrable f c R ↔
    IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
refine ⟨fun h => h.out, fun h => ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h : IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
neg :
  ∀
    (h :
      IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace)
        (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume),
    IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ CircleIntegrable f c R

Tactic:
simp only [CircleIntegrable, intervalIntegrable_iff, deriv_circleMap] at h ⊢

Premises used: intervalIntegrable_iff, deriv_circleMap, CircleIntegrable
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h :
  IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (Ι 0 (2 * π)) volume

Tactic:
(h.norm.const_mul |R|⁻¹).mono' ?_ ?_

Premises used: abs, MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono', MeasureTheory.IntegrableOn, Inv.inv, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h :
  IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume
neg :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ))
    (Measure.restrict volume (Ι 0 (2 * π)))
neg₁ :
  ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ι 0 (2 * π)),
    ‖f (circleMap c R a)‖ ≤ |R|⁻¹ * ‖(circleMap 0 R a * I) • f (circleMap c R a)‖
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (Ι 0 (2 * π)) volume

Tactic:
refine (h.norm.const_mul |R|⁻¹).mono' ?_ ?_

Premises used: abs, MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono', Inv.inv, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h :
  IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume
θ : ℝ
⊢ circleMap 0 R θ * I ≠ 0

Tactic:
simp [h₀, I_ne_zero]

Premises used: Complex.I_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h :
  IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ ∀ {θ : ℝ}, circleMap 0 R θ * I ≠ 0

Tactic:
have H : ∀ {θ}, circleMap 0 R θ * I ≠ 0 := fun {θ} => by simp [h₀, I_ne_zero]
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h :
  IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume
H : ∀ {θ : ℝ}, circleMap 0 R θ * I ≠ 0
⊢ AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ))
    (Measure.restrict volume (Ι 0 (2 * π)))

Tactic:
simpa only [inv_smul_smul₀ H]
      using ((continuous_circleMap 0 R).aestronglyMeasurable.mul_const
        I).aemeasurable.inv.aestronglyMeasurable.smul h.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, inv_smul_smul₀, continuous_circleMap, MeasureTheory.AEStronglyMeasurable.mul_const, AEMeasurable.inv, OfNat.ofNat, Continuous.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.smul, Complex.I
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h :
  IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ι 0 (2 * π)),
    ‖f (circleMap c R a)‖ ≤ |R|⁻¹ * ‖(circleMap 0 R a * I) • f (circleMap c R a)‖

Tactic:
simp [norm_smul, h₀]

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
hf : ContinuousOn f (sphere c |R|)
⊢ CircleIntegrable f c R

Tactic:
(hf.comp_continuous (continuous_circleMap _ _) (circleMap_mem_sphere' _ _)).intervalIntegrable _ _

Premises used: ContinuousOn.comp_continuous, continuous_circleMap, Continuous.intervalIntegrable, CircleIntegrable, circleMap_mem_sphere'
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
hR : 0 ≤ R
hf : ContinuousOn f (sphere c R)
⊢ CircleIntegrable f c R

Tactic:
ContinuousOn.circleIntegrable' <| (abs_of_nonneg hR).symm ▸ hf

Premises used: Eq.rec, abs_of_nonneg, ContinuousOn.circleIntegrable', Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
n : ℤ
mp : CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R → R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|
mpr : R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R| → CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
⊢ CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
n : ℤ
h : CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
mp : ∀ (h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c |R|), ¬CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
⊢ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|

Tactic:
contrapose! h
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c |R|
⊢ R ≠ 0

Tactic:
rcases h with ⟨hR, hn, hw⟩
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c |R|
hR : R ≠ 0
⊢ n < 0

Tactic:
rcases h with ⟨hR, hn, hw⟩
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c |R|
hR : R ≠ 0
hn : n < 0
⊢ w ∈ sphere c |R|

Tactic:
rcases h with ⟨hR, hn, hw⟩
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c |R|
mp : ¬IntervalIntegrable (ε := ℂ) (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)
⊢ ¬CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R

Tactic:
simp only [circleIntegrable_iff R, deriv_circleMap]

Premises used: circleIntegrable_iff, deriv_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c |R|
⊢ w ∈ circleMap c R '' Ioc 0 (2 * π)

Tactic:
rw [← image_circleMap_Ioc] at hw

Premises used: image_circleMap_Ioc
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ circleMap c R '' Ioc 0 (2 * π)
mp :
  ∀ (θ : ℝ) (hθ : θ ∈ Ioc 0 (2 * π)),
    ¬IntervalIntegrable (ε := ℂ) (fun (θ_1 : ℝ) ↦ (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n)
        volume 0 (2 * π)
⊢ ¬IntervalIntegrable (ε := ℂ) (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)

Tactic:
rcases hw with ⟨θ, hθ, rfl⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ Ioc 0 (2 * π)
⊢ θ ∈ [[0, 2 * π]]

Tactic:
replace hθ : θ ∈ [[0, 2 * π]] := Icc_subset_uIcc (Ioc_subset_Icc_self hθ)
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
⊢ ¬IntervalIntegrable (ε := ℂ) (fun (θ_1 : ℝ) ↦ (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n)
      volume 0 (2 * π)

Tactic:
not_intervalIntegrable_of_sub_inv_isBigO_punctured ?_ Real.two_pi_pos.ne hθ

Premises used: Real.two_pi_pos, not_intervalIntegrable_of_sub_inv_isBigO_punctured, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
mp :
  IsBigO (E := ℝ) (F := ℂ) (𝓝[≠] θ) (fun (x : ℝ) ↦ (x - θ)⁻¹) fun (θ_1 : ℝ) ↦
    (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
⊢ ¬IntervalIntegrable (ε := ℂ) (fun (θ_1 : ℝ) ↦ (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n)
      volume 0 (2 * π)

Tactic:
refine not_intervalIntegrable_of_sub_inv_isBigO_punctured ?_ Real.two_pi_pos.ne hθ

Premises used: Real.two_pi_pos, not_intervalIntegrable_of_sub_inv_isBigO_punctured, LT.lt.ne
-- 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 θ
suffices : ∀ᶠ (z : ℂ) in 𝓝[≠] circleMap c R θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (z - circleMap c R θ)
⊢ ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')

Tactic:
suffices ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0} from
        ((differentiable_circleMap c R θ).hasDerivAt.tendsto_nhdsNE
          (deriv_circleMap_ne_zero hR)).eventually this
-- 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 θ
h :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ) {circleMap c R θ}ᶜ a →
      a ∈ ball (circleMap c R θ) 1 → Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (a - circleMap c R θ)
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] circleMap c R θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (z - circleMap c R θ)

Tactic:
filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]

Premises used: mem_nhdsWithin_of_mem_nhds, Metric.ball_mem_nhds, zero_lt_one, self_mem_nhdsWithin
-- 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 θ
⊢ ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ) {circleMap c R θ}ᶜ a →
      a ∈ ball (circleMap c R θ) 1 → Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (a - circleMap c R θ)

Tactic:
simp_all [dist_eq, sub_eq_zero]

Premises used: sub_eq_zero, Complex.dist_eq
-- 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 θ
⊢ ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')

Tactic:
have : ∀ᶠ θ' in 𝓝[≠] θ, f θ' ∈ ball (0 : ℂ) 1 \ {0} := by
      suffices ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0} from
        ((differentiable_circleMap c R θ).hasDerivAt.tendsto_nhdsNE
          (deriv_circleMap_ne_zero hR)).eventually this
      filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]
      simp_all [dist_eq, sub_eq_zero]
-- 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 : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
⊢ IsBigO (E := ℝ) (F := ℂ) (𝓝[≠] θ) (fun (x : ℝ) ↦ (x - θ)⁻¹) fun (θ_1 : ℝ) ↦
    (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n

Tactic:
(((hasDerivAt_circleMap c R θ).isBigO_sub.mono inf_le_left).inv_rev
      (this.mono fun θ' h₁ h₂ => absurd h₂ h₁.2)).trans ?_

Premises used: Set.Mem, nhdsWithin, setOf, HasDerivAt.isBigO_sub, Asymptotics.IsBigO.trans, hasDerivAt_circleMap, Filter.Eventually.mono, absurd, And.right, Asymptotics.IsBigO.inv_rev, Asymptotics.IsBigO.mono, inf_le_left
-- 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 : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
mp :
  IsBigO (E := ℂ) (F := ℂ) (𝓝 θ ⊓ 𝓟 {θ}ᶜ) (fun (x : ℝ) ↦ (circleMap c R x - circleMap c R θ)⁻¹) fun (θ_1 : ℝ) ↦
    (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
⊢ IsBigO (E := ℝ) (F := ℂ) (𝓝[≠] θ) (fun (x : ℝ) ↦ (x - θ)⁻¹) fun (θ_1 : ℝ) ↦
    (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n

Tactic:
refine (((hasDerivAt_circleMap c R θ).isBigO_sub.mono inf_le_left).inv_rev
      (this.mono fun θ' h₁ h₂ => absurd h₂ h₁.2)).trans ?_

Premises used: HasDerivAt.isBigO_sub, Asymptotics.IsBigO.trans, hasDerivAt_circleMap, Filter.Eventually.mono, absurd, And.right, Asymptotics.IsBigO.inv_rev, Asymptotics.IsBigO.mono, inf_le_left
-- 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 : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 θ ⊓ 𝓟 {θ}ᶜ) (fun (x : ℝ) ↦ (circleMap c R x - circleMap c R θ)⁻¹) fun (θ_1 : ℝ) ↦
    (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n

Tactic:
IsBigO.of_bound |R|⁻¹ (this.mono fun θ' hθ' => ?_)

Premises used: abs, Filter.Eventually.mono, Inv.inv, Asymptotics.IsBigO.of_bound
-- 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 : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
mp :
  ∀ (θ' : ℝ) (hθ' : Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')),
    ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤
      |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 θ ⊓ 𝓟 {θ}ᶜ) (fun (x : ℝ) ↦ (circleMap c R x - circleMap c R θ)⁻¹) fun (θ_1 : ℝ) ↦
    (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n

Tactic:
refine IsBigO.of_bound |R|⁻¹ (this.mono fun θ' hθ' => ?_)

Premises used: abs, Filter.Eventually.mono, Inv.inv, Asymptotics.IsBigO.of_bound
-- 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 : x⁻¹ ≤ x ^ n
simp :
  ‖circleMap c R θ' - circleMap c R θ‖⁻¹ ≤ |R|⁻¹ * (‖circleMap 0 R θ'‖ * ‖(circleMap c R θ' - circleMap c R θ) ^ n‖)
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖

Tactic:
simp only [smul_eq_mul, norm_mul,
        norm_inv, norm_I, mul_one]

Premises used: norm_mul, norm_inv, Complex.norm_I, smul_eq_mul, mul_one
-- 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 : x⁻¹ ≤ x ^ n
⊢ ‖circleMap c R θ' - circleMap c R θ‖⁻¹ ≤ |R|⁻¹ * (‖circleMap 0 R θ'‖ * ‖(circleMap c R θ' - circleMap c R θ) ^ n‖)

Tactic:
simpa only [norm_circleMap_zero, norm_zpow, Ne, abs_eq_zero.not.2 hR, not_false_iff,
        inv_mul_cancel_left₀] using this

Premises used: Iff.mpr, norm_circleMap_zero, inv_mul_cancel_left₀, Iff.not, Ne, abs_eq_zero, norm_zpow, not_false_iff
-- 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 : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
θ' : ℝ
hθ' : Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
x : ℝ := ‖f θ'‖
mp : x⁻¹ ≤ x ^ n
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖

Tactic:
suffices x⁻¹ ≤ x ^ n by
      simp only [smul_eq_mul, norm_mul,
        norm_inv, norm_I, mul_one]
      simpa only [norm_circleMap_zero, norm_zpow, Ne, abs_eq_zero.not.2 hR, not_false_iff,
        inv_mul_cancel_left₀] using this
-- 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 : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
θ' : ℝ
hθ' : Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
x : ℝ := ‖f θ'‖
⊢ Membership.mem (γ := Set ℝ) (Ioo 0 1) x

Tactic:
simpa [x, and_comm] using hθ'

Premises used: and_comm
-- 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 : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
θ' : ℝ
hθ' : Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (f θ')
x : ℝ := ‖f θ'‖
⊢ Membership.mem (γ := Set ℝ) (Ioo 0 1) x

Tactic:
have : x ∈ Ioo (0 : ℝ) 1 := by simpa [x, and_comm] using hθ'
-- 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
mp : HPow.hPow (β := ℤ) x (-1) ≤ x ^ n
⊢ x⁻¹ ≤ x ^ n

Tactic:
rw [← zpow_neg_one]

Premises used: zpow_neg_one
-- 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
⊢ HPow.hPow (β := ℤ) x (-1) ≤ x ^ n

Tactic:
(zpow_right_strictAnti₀ this.1 this.2).le_iff_ge.2 (Int.lt_add_one_iff.1 ?_)

Premises used: Iff.mpr, And.right, StrictAnti.le_iff_ge, And.left, Iff.mp, Int.lt_add_one_iff, zpow_right_strictAnti₀
-- 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
mp : n < HAdd.hAdd (α := ℤ) (-1) 1
⊢ HPow.hPow (β := ℤ) x (-1) ≤ x ^ n

Tactic:
refine (zpow_right_strictAnti₀ this.1 this.2).le_iff_ge.2 (Int.lt_add_one_iff.1 ?_)

Premises used: Iff.mpr, And.right, StrictAnti.le_iff_ge, And.left, Iff.mp, Int.lt_add_one_iff, zpow_right_strictAnti₀