awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
rw : c +ᵥ sphere (HSMul.hSMul (β := ℂ) R 0) (‖R‖ * 1) = sphere c |R|
⊢ c +ᵥ HSMul.hSMul (β := Set ℂ) R (range fun (θ : ℝ) ↦ cexp ((↑θ : ℂ) * I)) = sphere c |R|

Tactic:
rw [range_exp_mul_I, smul_sphere R 0 zero_le_one]

Premises used: smul_sphere, zero_le_one, OfNat.ofNat, Complex.range_exp_mul_I
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
⊢ c +ᵥ sphere (HSMul.hSMul (β := ℂ) R 0) (‖R‖ * 1) = sphere c |R|

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
rw : circleMap c R '' Ioc 0 (2 * π) = range (circleMap c R)
rw₁ : circleMap c R '' Ioc 0 (2 * π) = circleMap c R '' Ioc 0 (0 + 2 * π)
rw₂ rw₃ : circleMap c R '' Ioc 0 (2 * π) = circleMap c R '' Ioc 0 (2 * π)
⊢ circleMap c R '' Ioc 0 (2 * π) = sphere c |R|

Tactic:
rw [← range_circleMap, ← (periodic_circleMap c R).image_Ioc Real.two_pi_pos 0, zero_add]

Premises used: range_circleMap, Real.two_pi_pos, zero_add, periodic_circleMap, Function.Periodic.image_Ioc, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R θ : ℝ
⊢ HasDerivAt (circleMap c R) (circleMap 0 R θ * I) θ

Tactic:
simpa only [mul_assoc, one_mul, ofRealCLM_apply, circleMap, ofReal_one, zero_add]
    using (((ofRealCLM.hasDerivAt (x := θ)).mul_const I).cexp.const_mul (R : ℂ)).const_add c

Premises used: ContinuousLinearMap.hasDerivAt, mul_assoc, circleMap, Complex.ofReal_one, Complex.ofRealCLM, Complex.ofRealCLM_apply, zero_add, Complex.ofReal, HasDerivAt.const_mul, HasDerivAt.const_add, HasDerivAt.cexp, one_mul, Complex.I, HasDerivAt.mul_const
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
⊢ Differentiable ℝ (circleMap c R)

Tactic:
fun θ =>
  (hasDerivAt_circleMap c R θ).differentiableAt

Premises used: Differentiable, HasDerivAt.differentiableAt, hasDerivAt_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R z : ℝ
hz : Membership.mem (γ := Set ℝ) univ z
apply : AnalyticAt ℝ (F := ℂ) (fun (θ : ℝ) ↦ (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) z
⊢ AnalyticAt ℝ (circleMap c R) z

Tactic:
apply analyticAt_const.add

Premises used: analyticAt_const, AnalyticAt.add
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R z : ℝ
hz : Membership.mem (γ := Set ℝ) univ z
apply : AnalyticAt ℝ (F := ℂ) (fun (θ : ℝ) ↦ cexp ((↑θ : ℂ) * I)) z
⊢ AnalyticAt ℝ (F := ℂ) (fun (θ : ℝ) ↦ (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) z

Tactic:
apply analyticAt_const.mul

Premises used: analyticAt_const, AnalyticAt.mul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R z : ℝ
hz : Membership.mem (γ := Set ℝ) univ z
⊢ AnalyticAt ℝ (F := ℂ) (fun (θ : ℝ) ↦ I) z

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R z : ℝ
hz : Membership.mem (γ := Set ℝ) univ z
⊢ AnalyticAt ℝ (cexp ∘ fun (θ : ℝ) ↦ (↑θ : ℂ) * I) z

Tactic:
apply analyticAt_cexp.restrictScalars.comp ((ofRealCLM.analyticAt z).mul (by fun_prop))

Premises used: ContinuousLinearMap.analyticAt, Complex.ofRealCLM, AnalyticAt.restrictScalars, AnalyticAt.mul, AnalyticAt.comp, analyticAt_cexp
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
n : WithTop ℕ∞
⊢ ContDiff ℝ n (circleMap c R)

Tactic:
(analyticOnNhd_circleMap c R).contDiff

Premises used: analyticOnNhd_circleMap, AnalyticOnNhd.contDiff
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
⊢ Continuous (circleMap c R)

Tactic:
(differentiable_circleMap c R).continuous

Premises used: Differentiable.continuous, differentiable_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
⊢ Measurable (circleMap c R)

Tactic:
(continuous_circleMap c R).measurable

Premises used: continuous_circleMap, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R θ : ℝ
⊢ deriv (circleMap c R) θ = circleMap 0 R θ * I

Tactic:
(hasDerivAt_circleMap _ _ _).deriv

Premises used: HasDerivAt.deriv, hasDerivAt_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R θ : ℝ
⊢ deriv (circleMap c R) θ = 0 ↔ R = 0

Tactic:
simp [I_ne_zero]

Premises used: Complex.I_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R θ : ℝ
hR : R ≠ 0
⊢ deriv (circleMap c R) θ ≠ 0

Tactic:
mt deriv_circleMap_eq_zero_iff.1 hR

Premises used: mt, Iff.mp, deriv_circleMap_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R θ : ℝ
⊢ (↑‖deriv (circleMap c R) θ‖₊ : ℝ) ≤ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) R) : ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
simp_rw : ∀ (θ : ℝ), circleMap z R θ ≠ w
⊢ ∀ (θ : ℝ), circleMap z R θ - w ≠ 0

Tactic:
simp_rw [sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ ≠ w

Tactic:
fun θ => circleMap_ne_mem_ball hw θ

Premises used: circleMap_ne_mem_ball
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ ≠ w

Tactic:
exact fun θ => circleMap_ne_mem_ball hw θ

Premises used: circleMap_ne_mem_ball
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ - w ≠ 0

Tactic:
have : ∀ θ, circleMap z R θ - w ≠ 0 := by
    simp_rw [sub_ne_zero]
    exact fun θ => circleMap_ne_mem_ball hw θ
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous (Y := ℂ) fun (θ : ℝ) ↦ circleMap z R θ - w

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous (Y := ℂ) fun (θ : ℝ) ↦ (circleMap z R θ - w)⁻¹

Tactic:
exact Continuous.inv₀ (by fun_prop) this

Premises used: Continuous.inv₀
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
h₂f : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) univ x → ¬EventuallyConst (circleMap c R) (𝓝 x)
hs₁ : s ∈ codiscreteWithin (circleMap c R '' univ)
⊢ s ∈ map (circleMap c R) (codiscrete ℝ)

Tactic:
apply (analyticOnNhd_circleMap c R).preimage_mem_codiscreteWithin

Premises used: analyticOnNhd_circleMap, AnalyticOnNhd.preimage_mem_codiscreteWithin
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
x : ℝ
hx : Membership.mem (γ := Set ℝ) univ x
h₂f : ∀ (hCon : EventuallyConst (circleMap c R) (𝓝 x)), False
⊢ ¬EventuallyConst (circleMap c R) (𝓝 x)

Tactic:
by_contra hCon
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
x : ℝ
hx : Membership.mem (γ := Set ℝ) univ x
hCon : EventuallyConst (circleMap c R) (𝓝 x)
h₂f : ∀ (a : ℂ) (ha : circleMap c R =ᶠ[𝓝 x] fun (x : ℝ) ↦ a), False
⊢ False

Tactic:
obtain ⟨a, ha⟩ := eventuallyConst_iff_exists_eventuallyEq.1 hCon

Premises used: Filter.eventuallyConst_iff_exists_eventuallyEq, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
x : ℝ
hx : Membership.mem (γ := Set ℝ) univ x
hCon : EventuallyConst (circleMap c R) (𝓝 x)
a : ℂ
ha : circleMap c R =ᶠ[𝓝 x] fun (x : ℝ) ↦ a
⊢ deriv (circleMap c R) x = deriv (fun (x : ℝ) ↦ a) x

Tactic:
have := ha.deriv.eq_of_nhds
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
x : ℝ
hx : Membership.mem (γ := Set ℝ) univ x
hCon : EventuallyConst (circleMap c R) (𝓝 x)
a : ℂ
ha : circleMap c R =ᶠ[𝓝 x] fun (x : ℝ) ↦ a
this : deriv (circleMap c R) x = deriv (fun (x : ℝ) ↦ a) x
⊢ False

Tactic:
simp [hR] at this
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
hs₁ : s ∈ codiscreteWithin (range (circleMap c R))
hs₂ hs₃ hs₄ hs₅ : s ∈ codiscreteWithin (sphere c |R|)
⊢ s ∈ codiscreteWithin (circleMap c R '' univ)

Tactic:
rwa [Set.image_univ, range_circleMap]

Premises used: Set.image_univ, range_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
r x : ℝ
c : ℂ
⊢ circleMap c (-r) x = circleMap c r (x + π)

Tactic:
simp [circleMap, add_mul, Complex.exp_add]

Premises used: add_mul, Complex.exp_add, circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
⊢ CircleIntegrable f c R ↔ IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
Iff.rfl

Premises used: Iff.rfl, CircleIntegrable
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : E
c : ℂ
R : ℝ
⊢ CircleIntegrable.{u_1} (E := E) (fun (x : ℂ) ↦ a) c R

Tactic:
intervalIntegrable_const

Premises used: CircleIntegrable, intervalIntegrable_const
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
hf : CircleIntegrable f c R
⊢ CircleIntegrable |f| c R

Tactic:
IntervalIntegrable.abs hf

Premises used: abs, CircleIntegrable, IntervalIntegrable.abs
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
hf : CircleIntegrable f c R
hg : CircleIntegrable g c R
⊢ CircleIntegrable (f + g) c R

Tactic:
IntervalIntegrable.add hf hg

Premises used: CircleIntegrable, IntervalIntegrable.add
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
hf : CircleIntegrable f c R
hg : CircleIntegrable g c R
⊢ CircleIntegrable (f - g) c R

Tactic:
IntervalIntegrable.sub hf hg

Premises used: IntervalIntegrable.sub, CircleIntegrable
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ Eq.{u_1 + 1} (α := (θ : ℝ) → E) (fun (θ : ℝ) ↦ (∑ i ∈ s, f i) (circleMap c R θ))
    (∑ i ∈ s, fun (θ : ℝ) ↦ f i (circleMap c R θ))

Tactic:
aesop
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
rw : IntervalIntegrable.{u_1} (ε := E) (∑ i ∈ s, fun (θ : ℝ) ↦ f i (circleMap c R θ)) volume 0 (2 * π)
⊢ CircleIntegrable.{u_1} (E := E) (∑ i ∈ s, f i) c R

Tactic:
rw [CircleIntegrable, (by aesop : (fun θ ↦ (∑ i ∈ s, f i) (circleMap c R θ))
    = ∑ i ∈ s, fun θ ↦ f i (circleMap c R θ))] at *

Premises used: CircleIntegrable
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ IntervalIntegrable.{u_1} (ε := E) (∑ i ∈ s, fun (θ : ℝ) ↦ f i (circleMap c R θ)) volume 0 (2 * π)

Tactic:
IntervalIntegrable.sum s h

Premises used: IntervalIntegrable.sum
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ IntervalIntegrable.{u_1} (ε := E) (∑ i ∈ s, fun (θ : ℝ) ↦ f i (circleMap c R θ)) volume 0 (2 * π)

Tactic:
exact IntervalIntegrable.sum s h

Premises used: IntervalIntegrable.sum
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ CircleIntegrable.{u_1} (E := E) (∑ i ∈ s, f i) c R

Tactic:
CircleIntegrable.sum s h

Premises used: CircleIntegrable.sum
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
h₁ : ∀ (x : ℂ), Eq.{u_1 + 1} (α := E) (∑ i ∈ s, f i x) ((∑ i ∈ s, f i) x)
⊢ CircleIntegrable.{u_1} (E := E) (fun (z : ℂ) ↦ ∑ i ∈ s, f i z) c R

Tactic:
convert! CircleIntegrable.sum s h

Premises used: CircleIntegrable.sum
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
x : ℂ
⊢ Eq.{u_1 + 1} (α := E) (∑ i ∈ s, f i x) ((∑ i ∈ s, f i) x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
pos : ∀ (h₁ : (support f).Finite), CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R
neg : ∀ (h₁ : ¬(support f).Finite), CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R
⊢ CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R

Tactic:
by_cases h₁ : (Function.support f).Finite

Premises used: Set.Finite, Function.support
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
h₁ : (support f).Finite
pos : CircleIntegrable.{u_1} (E := E) (∑ i ∈ h₁.toFinset (s := support f), f i) c R
⊢ CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R

Tactic:
rw [finsum_eq_sum f h₁]

Premises used: finsum_eq_sum
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
h₁ : (support f).Finite
⊢ CircleIntegrable.{u_1} (E := E) (∑ i ∈ h₁.toFinset (s := support f), f i) c R

Tactic:
CircleIntegrable.sum h₁.toFinset (fun i _ ↦ h i)

Premises used: CircleIntegrable.sum, Set.Finite.toFinset
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
h₁ : (support f).Finite
⊢ CircleIntegrable.{u_1} (E := E) (∑ i ∈ h₁.toFinset (s := support f), f i) c R

Tactic:
exact CircleIntegrable.sum h₁.toFinset (fun i _ ↦ h i)

Premises used: CircleIntegrable.sum, Set.Finite.toFinset
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
h₁ : ¬(support f).Finite
neg : CircleIntegrable.{u_1} (E := E) 0 c R
⊢ CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R

Tactic:
rw [finsum_of_infinite_support h₁]

Premises used: finsum_of_infinite_support
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
h₁ : ¬(support f).Finite
⊢ CircleIntegrable.{u_1} (E := E) 0 c R

Tactic:
apply circleIntegrable_const

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

Tactic:
hf.neg

Premises used: IntervalIntegrable.neg, CircleIntegrable
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
A : Type u_2
inst : NormedRing A
a : A
f : ℂ → A
h : CircleIntegrable f c R
⊢ CircleIntegrable (a • f) c R

Tactic:
IntervalIntegrable.const_mul h _

Premises used: CircleIntegrable, IntervalIntegrable.const_mul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
A : Type u_2
inst : NormedRing A
a : A
f : ℂ → A
h : CircleIntegrable f c R
⊢ CircleIntegrable.{u_2} (E := A) (fun (z : ℂ) ↦ a • f z) c R

Tactic:
const_smul h

Premises used: CircleIntegrable.const_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
𝕜 : Type u_3
F : Type u_4
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
f : ℂ → F
g : ℂ → 𝕜
hf : CircleIntegrable f c R
hg : ContinuousOn g (sphere c |R|)
⊢ ContinuousOn (circleMap c R) [[0, 2 * π]]

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
𝕜 : Type u_3
inst : NormedRing 𝕜
f g : ℂ → 𝕜
hf : CircleIntegrable f c R
hg : ContinuousOn g (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
f : ℂ → E
c : ℂ
R : ℝ
inst_1 : NormedSpace ℂ E
hf : CircleIntegrable f c R
simp :
  ∀
    (hf :
      IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (Ι 0 (2 * π))
        volume),
    IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace)
      (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
simp only [CircleIntegrable, deriv_circleMap, intervalIntegrable_iff] at *

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

Tactic:
(hf.norm.const_mul |R|).mono' ?_ ?_

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

Tactic:
refine (hf.norm.const_mul |R|).mono' ?_ ?_

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

Tactic:
((continuous_circleMap _ _).aestronglyMeasurable.mul_const I).smul hf.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, continuous_circleMap, MeasureTheory.AEStronglyMeasurable.mul_const, Continuous.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.smul, Complex.I
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst_1 : NormedSpace ℂ E
hf :
  IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace)
    (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Measure.restrict volume (Ι 0 (2 * π)))

Tactic:
exact ((continuous_circleMap _ _).aestronglyMeasurable.mul_const I).smul hf.aestronglyMeasurable

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

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
c : ℂ
⊢ CircleIntegrable f c 0

Tactic:
simp [CircleIntegrable]

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

Tactic:
intervalIntegrable_congr fun x _ ↦ hf (circleMap_mem_sphere' c R x)

Premises used: CircleIntegrable, intervalIntegrable_congr, circleMap_mem_sphere'
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
f : ℂ → E
x : ℝ
h : x ∈ Ι 0 (2 * π)
⊢ Eq.{u_1 + 1} (α := E) ((fun (θ : ℝ) ↦ f (circleMap c (-R) θ)) x) ((fun (θ : ℝ) ↦ (f ∘ circleMap c R) (θ + π)) x)

Tactic:
simp [circleMap_neg_radius]

Premises used: circleMap_neg_radius
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
f : ℂ → E
rw :
  IntervalIntegrable (f ∘ circleMap c R) volume (0 + π) (π + 2 * π) ↔
    IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ f (circleMap c R θ)) volume 0 (2 * π)
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ 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 * π) π]

Premises used: Real.pi, HMul.hMul, add_comm, IntervalIntegrable.comp_add_right_iff, intervalIntegrable_congr, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
f : ℂ → E
⊢ IntervalIntegrable (f ∘ circleMap c R) volume (0 + π) (π + 2 * π) ↔
    IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
simpa using ((periodic_circleMap c R).comp f).intervalIntegrable_iff (t₂ := 0)

Premises used: Function.Periodic.intervalIntegrable_iff, periodic_circleMap, Function.Periodic.comp
-- 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
pos : ∀ (hR : R = 0), CircleIntegrable f₂ c R
neg : ∀ (hR : ¬R = 0), CircleIntegrable f₂ c R
⊢ CircleIntegrable f₂ c R

Tactic:
by_cases hR : R = 0
-- 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
⊢ CircleIntegrable f₂ c R

Tactic:
simp [hR]
-- 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
apply :
  EventuallyEq.{0, u_1} (β := E) (codiscreteWithin (Ι 0 (2 * π))) (fun (θ : ℝ) ↦ f₁ (circleMap c R θ)) fun (θ : ℝ) ↦
    f₂ (circleMap c R θ)
⊢ CircleIntegrable f₂ c R

Tactic:
apply (intervalIntegrable_congr_codiscreteWithin _).1 hf₁

Premises used: intervalIntegrable_congr_codiscreteWithin, Iff.mp