awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
rw : circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x))
⊢ circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R (θ + η)))

Tactic:
rw [intervalIntegral.integral_comp_add_right (fun θ ↦ f (circleMap c R θ))]

Premises used: circleMap, intervalIntegral.integral_comp_add_right
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η x : ℝ
⊢ Eq.{u_1 + 1} (α := E) ((fun (θ : ℝ) ↦ f (circleMap c R θ)) (x + 2 * π)) ((fun (θ : ℝ) ↦ f (circleMap c R θ)) x)

Tactic:
simp [periodic_circleMap c R x]

Premises used: periodic_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
⊢ Function.Periodic.{0, u_1} (β := E) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (2 * π)

Tactic:
have t₀ : (fun θ ↦ f (circleMap c R θ)).Periodic (2 * π) :=
    fun x ↦ by simp [periodic_circleMap c R x]
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic.{0, u_1} (β := E) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (2 * π)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in 0..0 + 2 * π, f (circleMap c R x))
    (∫ (x : ℝ) in η..η + 2 * π, f (circleMap c R x))

Tactic:
have := t₀.intervalIntegral_add_eq 0 η
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic.{0, u_1} (β := E) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (2 * π)
this :
  Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in 0..0 + 2 * π, f (circleMap c R x))
    (∫ (x : ℝ) in η..η + 2 * π, f (circleMap c R x))
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in 0..2 * π, f (circleMap c R x)) (∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x))

Tactic:
rw [zero_add, add_comm] at this

Premises used: zero_add, add_comm
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic.{0, u_1} (β := E) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (2 * π)
this :
  Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in 0..2 * π, f (circleMap c R x)) (∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x))
rw : circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x))
⊢ circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x))

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic.{0, u_1} (β := E) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (2 * π)
this :
  Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in 0..2 * π, f (circleMap c R x)) (∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x))
simp :
  HSMul.hSMul (β := E) (π⁻¹ * 2⁻¹) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) =
    HSMul.hSMul (β := E) (π⁻¹ * 2⁻¹) (∫ (θ : ℝ) in η..2 * π + η, f (circleMap c R θ))
⊢ circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x))

Tactic:
simp only [circleAverage, mul_inv_rev]

Premises used: mul_inv_rev, Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic.{0, u_1} (β := E) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (2 * π)
this :
  Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in 0..2 * π, f (circleMap c R x)) (∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x))
⊢ HSMul.hSMul (β := E) (π⁻¹ * 2⁻¹) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) =
    HSMul.hSMul (β := E) (π⁻¹ * 2⁻¹) (∫ (θ : ℝ) in η..2 * π + η, f (circleMap c R θ))

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
unfold :
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c (-R) θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
⊢ circleAverage f c (-R) = circleAverage f c R

Tactic:
unfold circleAverage

Premises used: Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
simp_rw :
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R (θ + π))) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
simp_rw₁ : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R (θ + π))) = circleAverage f c R
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c (-R) θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))

Tactic:
simp_rw [circleMap_neg_radius, ← circleAverage_def, circleAverage_eq_integral_add π]

Premises used: Real.pi, Real.circleAverage_def, Real.circleAverage_eq_integral_add, circleMap_neg_radius
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
pos : ∀ (hR : 0 ≤ R), circleAverage f c |R| = circleAverage f c R
neg : ∀ (hR : R < 0), circleAverage f c |R| = circleAverage f c R
⊢ circleAverage f c |R| = circleAverage f c R

Tactic:
by_cases! hR : 0 ≤ R
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
hR : 0 ≤ R
pos pos₁ : circleAverage f c R = circleAverage f c R
⊢ circleAverage f c |R| = circleAverage f c R

Tactic:
rw [abs_of_nonneg hR]

Premises used: abs_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
hR : R < 0
neg : circleAverage f c (-R) = circleAverage f c R
neg₁ neg₂ : circleAverage f c R = circleAverage f c R
⊢ circleAverage f c |R| = circleAverage f c R

Tactic:
rw [abs_of_neg hR, circleAverage_neg_radius]

Premises used: abs_of_neg, Real.circleAverage_neg_radius
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
unfold :
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
⊢ circleAverage f₁ c R = circleAverage f₂ c R

Tactic:
unfold circleAverage

Premises used: Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
e_a : Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
e_a :
  EventuallyEq.{0, u_1} (β := E)
    (MeasureTheory.ae (F := MeasureTheory.Measure ℝ)
      (MeasureTheory.Measure.restrict MeasureTheory.volume (uIoc 0 (2 * π))))
    (fun (x : ℝ) ↦ f₁ (circleMap c R x)) fun (x : ℝ) ↦ f₂ (circleMap c R x)
⊢ Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))

Tactic:
apply intervalIntegral.integral_congr_ae_restrict

Premises used: intervalIntegral.integral_congr_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
e_a :
  {x : ℝ |
      (fun (x : ℝ) ↦
          Eq.{u_1 + 1} (α := E) ((fun (x : ℝ) ↦ f₁ (circleMap c R x)) x) ((fun (x : ℝ) ↦ f₂ (circleMap c R x)) x))
        x} ∈
    codiscreteWithin (uIoc 0 (2 * π))
⊢ EventuallyEq.{0, u_1} (β := E)
    (MeasureTheory.ae (F := MeasureTheory.Measure ℝ)
      (MeasureTheory.Measure.restrict MeasureTheory.volume (uIoc 0 (2 * π))))
    (fun (x : ℝ) ↦ f₁ (circleMap c R x)) fun (x : ℝ) ↦ f₂ (circleMap c R x)

Tactic:
apply ae_restrict_le_codiscreteWithin measurableSet_uIoc

Premises used: measurableSet_uIoc, ae_restrict_le_codiscreteWithin
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ ⦃a : ℝ⦄, a ∈ uIoc 0 (2 * π) → Membership.mem (γ := Set ℝ) univ a
⊢ uIoc 0 (2 * π) ⊆ univ

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ {x : ℝ |
      (fun (x : ℝ) ↦
          Eq.{u_1 + 1} (α := E) ((fun (x : ℝ) ↦ f₁ (circleMap c R x)) x) ((fun (x : ℝ) ↦ f₂ (circleMap c R x)) x))
        x} ∈
    codiscreteWithin (uIoc 0 (2 * π))

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

Premises used: Filter.codiscreteWithin_mono, circleMap_preimage_codiscrete
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : EqOn f₁ f₂ (sphere c |R|)
unfold :
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
⊢ circleAverage f₁ c R = circleAverage f₂ c R

Tactic:
unfold circleAverage

Premises used: Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : EqOn f₁ f₂ (sphere c |R|)
e_a : Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : EqOn f₁ f₂ (sphere c |R|)
x : ℝ
⊢ x ∈ uIcc 0 (2 * π) → f₁ (circleMap c R x) = f₂ (circleMap c R x)

Tactic:
simp [hf (circleMap_mem_sphere' c R x)]

Premises used: circleMap_mem_sphere'
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : EqOn f₁ f₂ (sphere c |R|)
⊢ Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))

Tactic:
exact intervalIntegral.integral_congr (fun x ↦ by simp [hf (circleMap_mem_sphere' c R x)])

Premises used: intervalIntegral.integral_congr
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
unfold :
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))) =
    HSMul.hSMul (β := E) (2 * π)⁻¹
      (∫ (θ : ℝ) in 0..2 * π, (fun (z : ℂ) ↦ f ((↑R : ℂ) * z + c)) (0 + (↑1 : ℂ) * cexp ((↑θ : ℂ) * I)))
⊢ circleAverage f c R = circleAverage (fun (z : ℂ) ↦ f ((↑R : ℂ) * z + c)) 0 1

Tactic:
unfold circleAverage circleMap

Premises used: circleMap, Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
e_a :
  ∀ (θ : ℝ),
    f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) = (fun (z : ℂ) ↦ f ((↑R : ℂ) * z + c)) (0 + (↑1 : ℂ) * cexp ((↑θ : ℂ) * I))
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))) =
    HSMul.hSMul (β := E) (2 * π)⁻¹
      (∫ (θ : ℝ) in 0..2 * π, (fun (z : ℂ) ↦ f ((↑R : ℂ) * z + c)) (0 + (↑1 : ℂ) * cexp ((↑θ : ℂ) * I)))

Tactic:
congr with θ
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R θ : ℝ
e_a : f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) = f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I) * (↑1 : ℂ))
⊢ f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) = (fun (z : ℂ) ↦ f ((↑R : ℂ) * z + c)) (0 + (↑1 : ℂ) * cexp ((↑θ : ℂ) * I))

Tactic:
ring_nf
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R θ : ℝ
⊢ f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) = f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I) * (↑1 : ℂ))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
unfold :
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (fun (x : ℂ) ↦ f x⁻¹) (circleMap 0 1 θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))
⊢ circleAverage (fun (x : ℂ) ↦ f x⁻¹) 0 1 = circleAverage f 0 1

Tactic:
unfold circleAverage

Premises used: Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
e_a :
  Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, (fun (x : ℂ) ↦ f x⁻¹) (circleMap 0 1 θ))
    (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (fun (x : ℂ) ↦ f x⁻¹) (circleMap 0 1 θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
⊢ Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ)⁻¹) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 (-θ)))

Tactic:
simp [circleMap_zero_inv]

Premises used: circleMap_zero_inv
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
rw : Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in -(2 * π)..-0, f (circleMap 0 1 x)) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))
⊢ Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 (-θ))) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))

Tactic:
rw [intervalIntegral.integral_comp_neg (fun w ↦ f (circleMap 0 1 w))]

Premises used: circleMap, OfNat.ofNat, intervalIntegral.integral_comp_neg
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
x : ℝ
⊢ Eq.{u_1 + 1} (α := E) ((fun (w : ℝ) ↦ f (circleMap 0 1 w)) (x + 2 * π)) ((fun (w : ℝ) ↦ f (circleMap 0 1 w)) x)

Tactic:
simp [periodic_circleMap 0 1 x]

Premises used: periodic_circleMap, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
⊢ Function.Periodic.{0, u_1} (β := E) (fun (w : ℝ) ↦ f (circleMap 0 1 w)) (2 * π)

Tactic:
have t₀ : Function.Periodic (fun w ↦ f (circleMap 0 1 w)) (2 * π) :=
      fun x ↦ by simp [periodic_circleMap 0 1 x]
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
t₀ : Function.Periodic.{0, u_1} (β := E) (fun (w : ℝ) ↦ f (circleMap 0 1 w)) (2 * π)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in -(2 * π)..-0, f (circleMap 0 1 x)) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))

Tactic:
simpa using (t₀.intervalIntegral_add_eq (-(2 * π)) 0)

Premises used: Real.pi, HMul.hMul, OfNat.ofNat, Function.Periodic.intervalIntegral_add_eq, Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
calc :
  Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ)⁻¹) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 (-θ)))
calc₁ :
  Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 (-θ))) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))
⊢ Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, (fun (x : ℂ) ↦ f x⁻¹) (circleMap 0 1 θ))
    (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))

Tactic:
calc ∫ θ in 0..2 * π, f (circleMap 0 1 θ)⁻¹
  _ = ∫ θ in 0..2 * π, f (circleMap 0 1 (-θ)) := by
    simp [circleMap_zero_inv]
  _ = ∫ θ in 0..2 * π, f (circleMap 0 1 θ) := by
    rw [intervalIntegral.integral_comp_neg (fun w ↦ f (circleMap 0 1 w))]
    have t₀ : Function.Periodic (fun w ↦ f (circleMap 0 1 w)) (2 * π) :=
      fun x ↦ by simp [periodic_circleMap 0 1 x]
    simpa using (t₀.intervalIntegral_add_eq (-(2 * π)) 0)
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
⊢ Continuous (Y := ℂ) fun (x : ℝ × ℝ) ↦ circleMap c x.1 x.2

Tactic:
fun_prop [circleMap]

Premises used: circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf : ContinuousOn f {z : ℂ | ‖z - c‖ ∈ s}
hs : ∀ r ∈ s, 0 ≤ r
rw :
  ∀
    (hf :
      Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (restrict («π» := fun (a : ℂ) ↦ E) {z : ℂ | ‖z - c‖ ∈ s} f))
    (hs : ∀ r ∈ s, 0 ≤ r),
    Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (s.restrict («π» := fun (a : ℝ) ↦ E) (Real.circleAverage f c))
⊢ ContinuousOn (Real.circleAverage f c) s

Tactic:
rw [continuousOn_iff_continuous_restrict] at *

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (restrict («π» := fun (a : ℂ) ↦ E) {z : ℂ | ‖z - c‖ ∈ s} f)
hs : ∀ r ∈ s, 0 ≤ r
apply :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Function.uncurry fun (x : (↑s : Type)) (t : ℝ) ↦ f (circleMap c (↑x : ℝ) t))
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (s.restrict («π» := fun (a : ℝ) ↦ E) (Real.circleAverage f c))

Tactic:
apply (intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' _ _ _).const_smul

Premises used: intervalIntegral.continuous_parametric_intervalIntegral_of_continuous', Continuous.const_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (restrict («π» := fun (a : ℂ) ↦ E) {z : ℂ | ‖z - c‖ ∈ s} f)
hs : ∀ r ∈ s, 0 ≤ r
x : (↑s : Type) × ℝ
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ s} (circleMap c (↑x.1 : ℝ) x.2)

Tactic:
simp [abs_of_nonneg (hs x.1 (Subtype.coe_prop x.1))]

Premises used: Subtype.coe_prop, Prod.fst, abs_of_nonneg, Subtype.val
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (restrict («π» := fun (a : ℂ) ↦ E) {z : ℂ | ‖z - c‖ ∈ s} f)
hs : ∀ r ∈ s, 0 ≤ r
⊢ ∀ (x : (↑s : Type) × ℝ), Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ s} (circleMap c (↑x.1 : ℝ) x.2)

Tactic:
have (x : s × ℝ) : circleMap c x.1 x.2 ∈ {z | ‖z - c‖ ∈ s} :=
    by simp [abs_of_nonneg (hs x.1 (Subtype.coe_prop x.1))]
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (restrict («π» := fun (a : ℂ) ↦ E) {z : ℂ | ‖z - c‖ ∈ s} f)
hs : ∀ r ∈ s, 0 ≤ r
this : ∀ (x : (↑s : Type) × ℝ), Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ s} (circleMap c (↑x.1 : ℝ) x.2)
apply :
  Continuous (Y := (↑{z : ℂ | ‖z - c‖ ∈ s} : Type)) fun (x : (↑s : Type) × ℝ) ↦
    Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ s} x) (circleMap c (↑x.1 : ℝ) x.2) ⋯
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Function.uncurry fun (x : (↑s : Type)) (t : ℝ) ↦ f (circleMap c (↑x : ℝ) t))

Tactic:
apply hf.comp (f := (fun x ↦ ⟨circleMap c x.1 x.2, this x⟩))

Premises used: Continuous.comp
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (restrict («π» := fun (a : ℂ) ↦ E) {z : ℂ | ‖z - c‖ ∈ s} f)
hs : ∀ r ∈ s, 0 ≤ r
this : ∀ (x : (↑s : Type) × ℝ), Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ s} (circleMap c (↑x.1 : ℝ) x.2)
⊢ Continuous (Y := (↑{z : ℂ | ‖z - c‖ ∈ s} : Type)) fun (x : (↑s : Type) × ℝ) ↦
    Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ s} x) (circleMap c (↑x.1 : ℝ) x.2) ⋯

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
f : ℂ → E
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
apply :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Function.uncurry fun (x t : ℝ) ↦ f (circleMap c x t))
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Real.circleAverage f c)

Tactic:
apply (intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' _ _ _).const_smul

Premises used: intervalIntegral.continuous_parametric_intervalIntegral_of_continuous', Continuous.const_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
f : ℂ → E
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Function.uncurry fun (x t : ℝ) ↦ f (circleMap c x t))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun (x : ℝ) ↦ c) (Ioo r R)
apply : 𝓝[<] R ≤ 𝓝[Ioc r R] R
⊢ Tendsto f (𝓝[<] R) (𝓝 (f R))

Tactic:
apply (h₁f R (right_mem_Ioc.mpr hR)).mono_left

Premises used: Iff.mpr, Set.right_mem_Ioc, Filter.Tendsto.mono_left
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun (x : ℝ) ↦ c) (Ioo r R)
rw : ∃ l ∈ Iio R, Ioo l R ⊆ Ioc r R
⊢ 𝓝[<] R ≤ 𝓝[Ioc r R] R

Tactic:
rw [nhdsWithin_le_iff, mem_nhdsLT_iff_exists_Ioo_subset]

Premises used: mem_nhdsLT_iff_exists_Ioo_subset, nhdsWithin_le_iff
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun (x : ℝ) ↦ c) (Ioo r R)
h : r ∈ Iio R ∧ Ioo r R ⊆ Ioc r R
⊢ ∃ l ∈ Iio R, Ioo l R ⊆ Ioc r R

Tactic:
use r
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun (x : ℝ) ↦ c) (Ioo r R)
⊢ r ∈ Iio R ∧ Ioo r R ⊆ Ioc r R

Tactic:
simp_all [Ioo_subset_Ioc_self]

Premises used: Set.Ioo_subset_Ioc_self
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun (x : ℝ) ↦ c) (Ioo r R)
⊢ Tendsto f (𝓝[<] R) (𝓝 (f R))

Tactic:
have : Filter.Tendsto f (𝓝[Iio R] R) (𝓝 (f R)) := by
    apply (h₁f R (right_mem_Ioc.mpr hR)).mono_left
    rw [nhdsWithin_le_iff, mem_nhdsLT_iff_exists_Ioo_subset]
    use r
    simp_all [Ioo_subset_Ioc_self]