awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
f : ℂ → E
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ f (circleMap c (-R) θ)) volume 0 (2 * π) ↔
    IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ f (circleMap c R θ)) volume 0 (2 * π)
have rw : IntervalIntegrable (f ∘ circleMap c R) volume (0 + π) (π + 2 * π) ↔
  IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ f (circleMap c R θ)) volume 0 (2 * π)
Tactic: rw [intervalIntegrable_congr (f := fun θ ↦ f (circleMap c (-R) θ))
    (g := fun θ ↦ (f ∘ (circleMap c R)) (θ + π)) (fun _ _ ↦ by simp [circleMap_neg_radius]),
    IntervalIntegrable.comp_add_right_iff (c := π), add_comm (2 * π) π]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
⊢ CircleIntegrable f₂ c R
have pos : ∀ (hR : R = 0), CircleIntegrable f₂ c R
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
pos : ∀ (hR : R = 0), CircleIntegrable f₂ c R
⊢ CircleIntegrable f₂ c R
have neg : ∀ (hR : ¬R = 0), CircleIntegrable f₂ c R
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
⊢ CircleIntegrable f₂ c R
have apply : EventuallyEq.{0, u_1} (β := E) (codiscreteWithin (Ι 0 (2 * π))) (fun (θ : ℝ) ↦ f₁ (circleMap c R θ)) fun (θ : ℝ) ↦
  f₂ (circleMap c R θ)
Tactic: apply (intervalIntegrable_congr_codiscreteWithin _).1 hf₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
⊢ EventuallyEq.{0, u_1} (β := E) (codiscreteWithin (Ι 0 (2 * π))) (fun (θ : ℝ) ↦ f₁ (circleMap c R θ)) fun (θ : ℝ) ↦
    f₂ (circleMap c R θ)
have rw : ∃ s ∈ codiscreteWithin (Ι 0 (2 * π)),
  EqOn.{0, u_1} (β := E) (fun (θ : ℝ) ↦ f₁ (circleMap c R θ)) (fun (θ : ℝ) ↦ f₂ (circleMap c R θ)) s
Tactic: rw [eventuallyEq_iff_exists_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
⊢ EqOn.{0, u_1} (β := E) (fun (θ : ℝ) ↦ f₁ (circleMap c R θ)) (fun (θ : ℝ) ↦ f₂ (circleMap c R θ))
    (circleMap c R ⁻¹' {z : ℂ | f₁ z = f₂ z})
have 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)
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ CircleIntegrable f c R ↔
    IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
have pos : ∀ (h₀ : R = 0),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 * π)
⊢ CircleIntegrable f c R ↔
    IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
have neg : ∀ (h₀ : ¬R = 0),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 * π)
have neg : ∀
  (h :
    IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)),
  CircleIntegrable f c R
Tactic: refine ⟨fun h => h.out, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 * π)
⊢ CircleIntegrable f c R
have 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
Tactic: simp only [CircleIntegrable, intervalIntegrable_iff, deriv_circleMap] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
have neg : AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ))
  (Measure.restrict volume (Ι 0 (2 * π)))
Tactic: refine (h.norm.const_mul |R|⁻¹).mono' ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 * π)))
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (Ι 0 (2 * π)) volume
have neg₁ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ι 0 (2 * π)),
  ‖f (circleMap c R a)‖ ≤ |R|⁻¹ * ‖(circleMap 0 R a * I) • f (circleMap c R a)‖
Tactic: refine (h.norm.const_mul |R|⁻¹).mono' ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
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
⊢ AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ))
    (Measure.restrict volume (Ι 0 (2 * π)))
have H : ∀ {θ : ℝ}, circleMap 0 R θ * I ≠ 0
Tactic: have H : ∀ {θ}, circleMap 0 R θ * I ≠ 0 := fun {θ} => by simp [h₀, I_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c w : ℂ
R : ℝ
n : ℤ
⊢ CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|
have mp : CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R → R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c w : ℂ
R : ℝ
n : ℤ
mp : CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R → R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|
⊢ CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|
have mpr : R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R| → CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c w : ℂ
R : ℝ
n : ℤ
h : CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
⊢ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|
have mp : ∀ (h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c |R|), ¬CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c |R|
⊢ ¬CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
have hR : R ≠ 0
Tactic: rcases h with ⟨hR, hn, hw⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c |R|
hR : R ≠ 0
⊢ ¬CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
have hn : n < 0
Tactic: rcases h with ⟨hR, hn, hw⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c |R|
hR : R ≠ 0
hn : n < 0
⊢ ¬CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
have hw : w ∈ sphere c |R|
Tactic: rcases h with ⟨hR, hn, hw⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c |R|
⊢ ¬CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
have mp : ¬IntervalIntegrable (ε := ℂ) (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)
Tactic: simp only [circleIntegrable_iff R, deriv_circleMap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c |R|
⊢ ¬IntervalIntegrable (ε := ℂ) (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)
have hw₁ : w ∈ circleMap c R '' Ioc 0 (2 * π)
Tactic: rw [← image_circleMap_Ioc] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ circleMap c R '' Ioc 0 (2 * π)
⊢ ¬IntervalIntegrable (ε := ℂ) (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)
have mp : ∀ (θ : ℝ) (hθ : θ ∈ Ioc 0 (2 * π)),
  ¬IntervalIntegrable (ε := ℂ) (fun (θ_1 : ℝ) ↦ (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n)
      volume 0 (2 * π)
Tactic: rcases hw with ⟨θ, hθ, rfl⟩
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ Ioc 0 (2 * π)
⊢ ¬IntervalIntegrable (ε := ℂ) (fun (θ_1 : ℝ) ↦ (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n)
      volume 0 (2 * π)
have hθ₁ : θ ∈ [[0, 2 * π]]
Tactic: replace hθ : θ ∈ [[0, 2 * π]] := Icc_subset_uIcc (Ioc_subset_Icc_self hθ)
Cleared hypotheses: hθ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 * π)
have mp : IsBigO (E := ℝ) (F := ℂ) (𝓝[≠] θ) (fun (x : ℝ) ↦ (x - θ)⁻¹) fun (θ_1 : ℝ) ↦
  (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
Tactic: refine not_intervalIntegrable_of_sub_inv_isBigO_punctured ?_ Real.two_pi_pos.ne hθ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 θ')
have suffices : ∀ᶠ (z : ℂ) in 𝓝[≠] circleMap c R θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (z - circleMap c R θ)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun (θ' : ℝ) ↦ circleMap c R θ' - circleMap c R θ
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] circleMap c R θ, Membership.mem (γ := Set ℂ) (ball 0 1 \ {0}) (z - circleMap c R θ)
have 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 θ)
Tactic: filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun (θ' : ℝ) ↦ circleMap c R θ' - circleMap c R θ
⊢ IsBigO (E := ℝ) (F := ℂ) (𝓝[≠] θ) (fun (x : ℝ) ↦ (x - θ)⁻¹) fun (θ_1 : ℝ) ↦
    (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
have this : ∀ᶠ (θ' : ℝ) 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
have 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
Tactic: refine (((hasDerivAt_circleMap c R θ).isBigO_sub.mono inf_le_left).inv_rev
      (this.mono fun θ' h₁ h₂ => absurd h₂ h₁.2)).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
have 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‖
Tactic: refine IsBigO.of_bound |R|⁻¹ (this.mono fun θ' hθ' => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
have simp : ‖circleMap c R θ' - circleMap c R θ‖⁻¹ ≤ |R|⁻¹ * (‖circleMap 0 R θ'‖ * ‖(circleMap c R θ' - circleMap c R θ) ^ n‖)
Tactic: simp only [smul_eq_mul, norm_mul,
        norm_inv, norm_I, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 θ'‖
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
have mp : x⁻¹ ≤ x ^ 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
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 θ'‖
⊢ x⁻¹ ≤ x ^ n
have this₁ : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
Tactic: have : x ∈ Ioo (0 : ℝ) 1 := by simpa [x, and_comm] using hθ'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
⊢ x⁻¹ ≤ x ^ n
have mp : HPow.hPow (β := ℤ) x (-1) ≤ x ^ n
Tactic: rw [← zpow_neg_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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
have mp : n < HAdd.hAdd (α := ℤ) (-1) 1
Tactic: refine (zpow_right_strictAnti₀ this.1 this.2).le_iff_ge.2 (Int.lt_add_one_iff.1 ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c w : ℂ
R : ℝ
⊢ CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w)⁻¹) c R ↔ R = 0 ∨ w ∉ sphere c |R|
have simp : R = 0 ∨ LE.le (α := ℤ) 0 (-1) ∨ w ∉ sphere c |R| ↔ R = 0 ∨ w ∉ sphere c |R|
Tactic: simp only [← zpow_neg_one, circleIntegrable_sub_zpow_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
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 θ))
have 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 θ))
Tactic: rw [circleIntegral, intervalIntegral.integral_of_le Real.two_pi_pos.le,
    Measure.restrict_congr_set Ioc_ae_eq_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 θ))
⊢ 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 θ))
have 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 θ))
Tactic: rw [circleIntegral, intervalIntegral.integral_of_le Real.two_pi_pos.le,
    Measure.restrict_congr_set Ioc_ae_eq_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 θ))
⊢ 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 θ))
have 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 θ))
Tactic: rw [circleIntegral, intervalIntegral.integral_of_le Real.two_pi_pos.le,
    Measure.restrict_congr_set Ioc_ae_eq_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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)
⊢ Tendsto.{u_2, u_1} (β := E) (fun (n : ι) ↦ ∮ (z : ℂ) in C(c, R), f n z) l (𝓝 (∮ (z : ℂ) in C(c, R), g z))
have 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 * π]]
Tactic: apply TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
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 * π]]
⊢ Tendsto.{u_2, u_1} (β := E) (fun (n : ι) ↦ ∮ (z : ℂ) in C(c, R), f n z) l (𝓝 (∮ (z : ℂ) in C(c, R), g z))
have 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 * π]]
Tactic: apply TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn