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
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 * π]]
have hF : ∀ (i : ι) (hi : ContinuousOn (f i) (sphere c R)), ContinuousOn (deriv (circleMap c R)) [[0, 2 * π]]
Tactic: refine hf.mono fun i hi ↦ .smul ?_ (hi.comp ?_ ?_)
-- 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 : ι) (hi : ContinuousOn (f i) (sphere c R)), ContinuousOn (deriv (circleMap c R)) [[0, 2 * π]]
⊢ ∀ᶠ (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 * π]]
have hF₁ : ∀ (i : ι) (hi : ContinuousOn (f i) (sphere c R)), ContinuousOn (circleMap c R) [[0, 2 * π]]
Tactic: refine hf.mono fun i hi ↦ .smul ?_ (hi.comp ?_ ?_)
-- 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 : ι) (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 * π]]
⊢ ∀ᶠ (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 * π]]
have hF₂ : ∀ (i : ι) (hi : ContinuousOn (f i) (sphere c R)), MapsTo (circleMap c R) [[0, 2 * π]] (sphere c R)
Tactic: refine hf.mono fun i hi ↦ .smul ?_ (hi.comp ?_ ?_)
-- 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)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ ContinuousOn (deriv (circleMap c R)) [[0, 2 * π]]
have hF : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ circleMap 0 R x * I) [[0, 2 * π]]
Tactic: rw [funext (deriv_circleMap _ _)]
-- 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)
⊢ 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 * π]]
have 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))) <
          ε
Tactic: rw [Metric.tendstoUniformlyOn_iff] 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
ι : 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) < ε
⊢ ∀ ε > 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))) <
          ε
have h_lim : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ [[0, 2 * π]], R * dist (g (circleMap c R x)) (f n (circleMap c R x)) < ε
Tactic: simp only [dist_smul₀, deriv_circleMap, norm_mul, norm_I, norm_circleMap_zero,
      abs_of_nonneg hR, mul_one]
-- 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 : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : ι) in l, ∀ x ∈ [[0, 2 * π]], R * dist (g (circleMap c R x)) (f n (circleMap c R x)) < ε
have 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)) < ε
Tactic: rcases exists_pos_mul_lt hε R with ⟨δ, hδ₀, hRδ⟩
-- 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 : ∀ ε > 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)) < ε
have 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)) < ε
Tactic: refine (h δ hδ₀).mono fun i hi x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), f₁ z) (∮ (z : ℂ) in C(c, R), f₂ z)
have 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))
Tactic: apply intervalIntegral.integral_congr_ae_restrict
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ (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))
have 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 * π))
Tactic: apply ae_restrict_le_codiscreteWithin measurableSet_uIoc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ {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 * π))
have h : {x : ℝ | f₁ (circleMap c R x) = f₂ (circleMap c R 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ Ι 0 (2 * π) ⊆ univ
have tauto : ∀ ⦃a : ℝ⦄, a ∈ Ι 0 (2 * π) → Membership.mem (γ := Set ℝ) univ a
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 w : ℂ
R : ℝ
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) (∮ (z : ℂ) in C(c, R), f z)
have inl : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, 0), (z - w)⁻¹ • (z - w) • f z) (∮ (z : ℂ) in C(c, 0), f z)
Tactic: rcases eq_or_ne R 0 with (rfl | hR)
Cleared hypotheses: R
-- 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 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)
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) (∮ (z : ℂ) in C(c, R), f z)
have 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)
Tactic: rcases eq_or_ne R 0 with (rfl | hR)
-- 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 w : ℂ
R : ℝ
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)
have this : (circleMap c R ⁻¹' {w}).Countable
Tactic: have : (circleMap c R ⁻¹' {w}).Countable := (countable_singleton _).preimage_circleMap c hR
-- 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 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)
have 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 θ))
Tactic: refine intervalIntegral.integral_congr_ae ((this.ae_notMem _).mono fun θ hθ _' => ?_)
-- 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 w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
θ : ℝ
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 θ))
have hθ₁ : circleMap c R θ ≠ w
Tactic: change circleMap c R θ ≠ w 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 C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
θ : ℝ
h : θ ∈ Ι 0 (2 * π)
⊢ |R| * ‖f (circleMap c R θ)‖ ≤ |R| * C
have hbc : ‖f (circleMap c R θ)‖ ≤ C
Tactic: gcongr
-- 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 C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
⊢ |R| * C * |2 * π - 0| = 2 * π * |R| * C
have rw : |R| * C * (2 * π) = 2 * π * |R| * C
Tactic: rw [sub_zero, _root_.abs_of_pos Real.two_pi_pos]
-- 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 C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : |R| = R
⊢ 2 * π * |R| * C = 2 * π * R * C
have rw : 2 * π * R * C = 2 * π * R * C
Tactic: rw [this]
-- 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 C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), f z)‖ ≤ R * C
have this : ‖(2 * (↑π : ℂ) * I)⁻¹‖ = (2 * π)⁻¹
Tactic: have : ‖(2 * π * I : ℂ)⁻¹‖ = (2 * π)⁻¹ := by simp [Real.pi_pos.le]
-- 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 C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * (↑π : ℂ) * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), f z)‖ ≤ R * C
have rw : norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) ≤ 2 * π * R * C
Tactic: rw [norm_smul, this, ← div_eq_inv_mul, div_le_iff₀ Real.two_pi_pos, mul_comm (R * C), ← mul_assoc]
-- 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 C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hlt : ∃ z ∈ sphere c R, ‖f z‖ < C
⊢ norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) < 2 * π * R * C
have hlt₁ : ∃ z ∈ circleMap c R '' Ioc 0 (2 * π), ‖f z‖ < C
Tactic: rw [← _root_.abs_of_pos hR, ← image_circleMap_Ioc] at hlt
Cleared hypotheses: hlt
-- 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 C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hlt : ∃ z ∈ circleMap c R '' Ioc 0 (2 * π), ‖f z‖ < C
⊢ norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) < 2 * π * R * C
have rcases : ∀ (θ₀ : ℝ) (hmem : θ₀ ∈ Ioc 0 (2 * π)) (hlt : ‖f (circleMap c R θ₀)‖ < C),
  norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) < 2 * π * R * C
Tactic: rcases hlt with ⟨_, ⟨θ₀, hmem, rfl⟩, hlt⟩
Cleared hypotheses: hlt
-- 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 C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)
have simp : LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, R * ‖f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)
Tactic: simp only [deriv_circleMap, norm_smul, norm_mul, norm_circleMap_zero, abs_of_pos hR, norm_I,
        mul_one]
-- 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 C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, R * ‖f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)
have refine_1 : ContinuousOn (Y := ℝ) (fun (θ : ℝ) ↦ R * ‖f (circleMap c R θ)‖) (Icc 0 (2 * π))
Tactic: refine intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
          Real.two_pi_pos ?_ continuousOn_const (fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩
-- 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 C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
refine_1 : ContinuousOn (Y := ℝ) (fun (θ : ℝ) ↦ R * ‖f (circleMap c R θ)‖) (Icc 0 (2 * π))
⊢ LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, R * ‖f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)
have refine_2 : ∀ θ ∈ Ioc 0 (2 * π), R * ‖f (circleMap c R θ)‖ ≤ R * C
Tactic: refine intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
          Real.two_pi_pos ?_ continuousOn_const (fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩
-- 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 C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
refine_1 : ContinuousOn (Y := ℝ) (fun (θ : ℝ) ↦ R * ‖f (circleMap c R θ)‖) (Icc 0 (2 * π))
refine_2 : ∀ θ ∈ Ioc 0 (2 * π), R * ‖f (circleMap c R θ)‖ ≤ R * C
⊢ LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, R * ‖f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)
have refine_3 : R * ‖f (circleMap c R θ₀)‖ < R * C
Tactic: refine intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
          Real.two_pi_pos ?_ continuousOn_const (fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩
-- 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 C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
θ : ℝ
h : θ ∈ Ioc 0 (2 * π)
⊢ R * ‖f (circleMap c R θ)‖ ≤ R * C
have refine_2 : ‖f (circleMap c R θ)‖ ≤ C
Tactic: gcongr
-- 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 C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ∫ (x : ℝ) in 0..2 * π, R * C = 2 * π * R * C
have simp : R * (2 * (π * C)) = 2 * (π * (R * C))
Tactic: simp [mul_assoc]
-- 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 C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) < 2 * π * R * C
have z : LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)
Tactic: calc
    ‖∮ z in C(c, R), f z‖ ≤ ∫ θ in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ :=
      intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le
    _ < ∫ _ in 0..2 * π, R * C := by
      simp only [deriv_circleMap, norm_smul, norm_mul, norm_circleMap_zero, abs_of_pos hR, norm_I,
        mul_one]
      refine intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
          Real.two_pi_pos ?_ continuousOn_const (fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩
      · exact continuousOn_const.mul (hc.comp (continuous_circleMap _ _).continuousOn fun θ _ =>
          circleMap_mem_sphere _ hR.le _).norm
      · gcongr
        exact hf _ <| circleMap_mem_sphere _ hR.le _
      · gcongr
    _ = 2 * π * R * C := by simp [mul_assoc]; ring
-- 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 C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
z :
  LT.lt (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖) (∫ (x : ℝ) in 0..2 * π, R * C)
⊢ norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), f z) < 2 * π * R * C
have z₁ : ∫ (x : ℝ) in 0..2 * π, R * C = 2 * π * R * C
Tactic: calc
    ‖∮ z in C(c, R), f z‖ ≤ ∫ θ in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ :=
      intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le
    _ < ∫ _ in 0..2 * π, R * C := by
      simp only [deriv_circleMap, norm_smul, norm_mul, norm_circleMap_zero, abs_of_pos hR, norm_I,
        mul_one]
      refine intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
          Real.two_pi_pos ?_ continuousOn_const (fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩
      · exact continuousOn_const.mul (hc.comp (continuous_circleMap _ _).continuousOn fun θ _ =>
          circleMap_mem_sphere _ hR.le _).norm
      · gcongr
        exact hf _ <| circleMap_mem_sphere _ hR.le _
      · gcongr
    _ = 2 * π * R * C := by simp [mul_assoc]; ring
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0
have pos : ∀ (hi : CircleIntegrable f' c R), Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0
Tactic: by_cases hi : CircleIntegrable f' c R
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
pos : ∀ (hi : CircleIntegrable f' c R), Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0
have neg : ∀ (hi : ¬CircleIntegrable f' c R), Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0
Tactic: by_cases hi : CircleIntegrable f' c R
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : CircleIntegrable f' c R
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, R), f' z) 0
have pos : ∮ (z : ℂ) in C(c, R), f' z = (f ∘ circleMap c R) (2 * π) - (f ∘ circleMap c R) 0
Tactic: rw [← sub_eq_zero.2 ((periodic_circleMap c R).comp f).eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : CircleIntegrable f' c R
⊢ ∮ (z : ℂ) in C(c, R), f' z = (f ∘ circleMap c R) (2 * π) - (f ∘ circleMap c R) 0
have pos : ∀ θ ∈ [[0, 2 * π]],
  HasDerivAt (f ∘ circleMap c R)
    (HSMul.hSMul (β := E) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ f' z) (circleMap c R θ))) θ
Tactic: refine intervalIntegral.integral_eq_sub_of_hasDerivAt (fun θ _ => ?_) hi.out
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
have inl : ∀ (hw : w ∈ sphere c |0|), Eq (α := ℂ) (∮ (z : ℂ) in C(c, 0), (z - w) ^ n) 0
Tactic: rcases eq_or_ne R 0 with (rfl | h0)
Cleared hypotheses: R, hw
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
inl : ∀ (hw : w ∈ sphere c |0|), Eq (α := ℂ) (∮ (z : ℂ) in C(c, 0), (z - w) ^ n) 0
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
have inr : ∀ (h0 : R ≠ 0), Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
Tactic: rcases eq_or_ne R 0 with (rfl | h0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
h0 : R ≠ 0
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0
have inr : ¬CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ (z - w) ^ n) c R
Tactic: apply integral_undef