awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ circleAverage f c R = HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z)
have calc : circleAverage f c R = HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
Tactic: calc circleAverage f c R
  _ = (↑(2 * π) : ℂ)⁻¹ • ∫ θ in 0..2 * π, f (circleMap c R θ) := by
    simp [circleAverage, ← coe_smul]
  _ = (2 * π * I)⁻¹ • ∫ θ in 0..2 * π, I • f (circleMap c R θ) := by
    rw [intervalIntegral.integral_smul, mul_inv_rev, smul_smul]
    match_scalars
    field
  _ = (2 * π * I)⁻¹ • (∮ z in C(c, R), (z - c)⁻¹ • f z) := by
    unfold circleIntegral
    congr with θ
    simp [deriv_circleMap, circleMap_sub_center, smul_smul]
    field_simp [circleMap_ne_center h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
calc : circleAverage f c R = HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
⊢ circleAverage f c R = HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z)
have calc₁ : HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) =
  HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c R θ))
Tactic: calc circleAverage f c R
  _ = (↑(2 * π) : ℂ)⁻¹ • ∫ θ in 0..2 * π, f (circleMap c R θ) := by
    simp [circleAverage, ← coe_smul]
  _ = (2 * π * I)⁻¹ • ∫ θ in 0..2 * π, I • f (circleMap c R θ) := by
    rw [intervalIntegral.integral_smul, mul_inv_rev, smul_smul]
    match_scalars
    field
  _ = (2 * π * I)⁻¹ • (∮ z in C(c, R), (z - c)⁻¹ • f z) := by
    unfold circleIntegral
    congr with θ
    simp [deriv_circleMap, circleMap_sub_center, smul_smul]
    field_simp [circleMap_ne_center h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
calc : circleAverage f c R = HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
calc₁ :
  HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) =
    HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c R θ))
⊢ circleAverage f c R = HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z)
have calc₂ : HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c R θ)) =
  HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z)
Tactic: calc circleAverage f c R
  _ = (↑(2 * π) : ℂ)⁻¹ • ∫ θ in 0..2 * π, f (circleMap c R θ) := by
    simp [circleAverage, ← coe_smul]
  _ = (2 * π * I)⁻¹ • ∫ θ in 0..2 * π, I • f (circleMap c R θ) := by
    rw [intervalIntegral.integral_smul, mul_inv_rev, smul_smul]
    match_scalars
    field
  _ = (2 * π * I)⁻¹ • (∮ z in C(c, R), (z - c)⁻¹ • f z) := by
    unfold circleIntegral
    congr with θ
    simp [deriv_circleMap, circleMap_sub_center, smul_smul]
    field_simp [circleMap_ne_center h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
⊢ circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R (θ + η)))
have rw : circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x))
Tactic: rw [intervalIntegral.integral_comp_add_right (fun θ ↦ f (circleMap c R θ))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
⊢ circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x))
have t₀ : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (hypothesis)
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 * π)
⊢ circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x))
have this : 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 η
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (hypothesis)
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))
⊢ circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x))
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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))
⊢ circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x))
have rw : circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x))
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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))
⊢ circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x))
have simp : HSMul.hSMul (β := E) (π⁻¹ * 2⁻¹) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) =
  HSMul.hSMul (β := E) (π⁻¹ * 2⁻¹) (∫ (θ : ℝ) in η..2 * π + η, f (circleMap c R θ))
Tactic: simp only [circleAverage, mul_inv_rev]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ circleAverage f c (-R) = circleAverage f c R
have unfold : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c (-R) θ)) =
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
Tactic: unfold circleAverage
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c (-R) θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
have simp_rw : 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 π]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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 θ))
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c (-R) θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
have simp_rw₁ : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R (θ + π))) = circleAverage f c R
Tactic: simp_rw [circleMap_neg_radius, ← circleAverage_def, circleAverage_eq_integral_add π]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ circleAverage f c |R| = circleAverage f c R
have pos : ∀ (hR : 0 ≤ R), circleAverage f c |R| = circleAverage f c R
Tactic: by_cases! hR : 0 ≤ R
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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
⊢ circleAverage f c |R| = circleAverage f c R
have neg : ∀ (hR : R < 0), circleAverage f c |R| = circleAverage f c R
Tactic: by_cases! hR : 0 ≤ R
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
hR : 0 ≤ R
⊢ circleAverage f c |R| = circleAverage f c R
have pos : circleAverage f c R = circleAverage f c R
Tactic: rw [abs_of_nonneg hR]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
hR : R < 0
⊢ circleAverage f c |R| = circleAverage f c R
have neg : circleAverage f c (-R) = circleAverage f c R
Tactic: rw [abs_of_neg hR, circleAverage_neg_radius]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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
⊢ circleAverage f c |R| = circleAverage f c R
have neg₁ : circleAverage f c R = circleAverage f c R
Tactic: rw [abs_of_neg hR, circleAverage_neg_radius]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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
⊢ circleAverage f₁ c R = circleAverage f₂ c R
have unfold : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) =
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
Tactic: unfold circleAverage
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
have e_a : Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
have 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)
Tactic: apply intervalIntegral.integral_congr_ae_restrict
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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
⊢ 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)
have 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 * π))
Tactic: apply ae_restrict_le_codiscreteWithin measurableSet_uIoc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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
⊢ uIoc 0 (2 * π) ⊆ univ
have tauto : ∀ ⦃a : ℝ⦄, a ∈ uIoc 0 (2 * π) → Membership.mem (γ := Set ℝ) univ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : EqOn f₁ f₂ (sphere c |R|)
⊢ circleAverage f₁ c R = circleAverage f₂ c R
have unfold : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) =
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
Tactic: unfold circleAverage
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : EqOn f₁ f₂ (sphere c |R|)
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
have e_a : Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ circleAverage f c R = circleAverage (fun (z : ℂ) ↦ f ((↑R : ℂ) * z + c)) 0 1
have 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)))
Tactic: unfold circleAverage circleMap
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ 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)))
have e_a : ∀ (θ : ℝ),
  f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) = (fun (z : ℂ) ↦ f ((↑R : ℂ) * z + c)) (0 + (↑1 : ℂ) * cexp ((↑θ : ℂ) * I))
Tactic: congr with θ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R θ : ℝ
⊢ f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) = (fun (z : ℂ) ↦ f ((↑R : ℂ) * z + c)) (0 + (↑1 : ℂ) * cexp ((↑θ : ℂ) * I))
have e_a : f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) = f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I) * (↑1 : ℂ))
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
⊢ circleAverage (fun (x : ℂ) ↦ f x⁻¹) 0 1 = circleAverage f 0 1
have 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 θ))
Tactic: unfold circleAverage
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
⊢ 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 θ))
have e_a : Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, (fun (x : ℂ) ↦ f x⁻¹) (circleMap 0 1 θ))
  (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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 θ))
have rw : Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in -(2 * π)..-0, f (circleMap 0 1 x)) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))
Tactic: rw [intervalIntegral.integral_comp_neg (fun w ↦ f (circleMap 0 1 w))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in -(2 * π)..-0, f (circleMap 0 1 x)) (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))
have t₀ : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
⊢ Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, (fun (x : ℂ) ↦ f x⁻¹) (circleMap 0 1 θ))
    (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))
have calc : Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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 (-θ)))
⊢ Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, (fun (x : ℂ) ↦ f x⁻¹) (circleMap 0 1 θ))
    (∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ))
have calc₁ : Eq.{u_1 + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, f (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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
⊢ ContinuousOn (Real.circleAverage f c) s
have 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))
Tactic: rw [continuousOn_iff_continuous_restrict] at *
Cleared hypotheses: hf, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (s.restrict («π» := fun (a : ℝ) ↦ E) (Real.circleAverage f c))
have apply : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (Function.uncurry fun (x : (↑s : Type)) (t : ℝ) ↦ f (circleMap c (↑x : ℝ) t))
Tactic: apply (intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' _ _ _).const_smul
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (hypothesis)
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
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Function.uncurry fun (x : (↑s : Type)) (t : ℝ) ↦ f (circleMap c (↑x : ℝ) t))
have this : ∀ (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))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Function.uncurry fun (x : (↑s : Type)) (t : ℝ) ↦ f (circleMap c (↑x : ℝ) t))
have 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) sorry
Tactic: apply hf.comp (f := (fun x ↦ ⟨circleMap c x.1 x.2, this x⟩))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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] (Real.circleAverage f c)
have apply : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (Function.uncurry fun (x t : ℝ) ↦ f (circleMap c x t))
Tactic: apply (intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' _ _ _).const_smul
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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))
have apply : 𝓝[<] R ≤ 𝓝[Ioc r R] R
Tactic: apply (h₁f R (right_mem_Ioc.mpr hR)).mono_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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 ≤ 𝓝[Ioc r R] R
have rw : ∃ l ∈ Iio R, Ioo l R ⊆ Ioc r R
Tactic: rw [nhdsWithin_le_iff, mem_nhdsLT_iff_exists_Ioo_subset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
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)
⊢ ∃ l ∈ Iio R, Ioo l R ⊆ Ioc r R
have h : r ∈ Iio R ∧ Ioo r R ⊆ Ioc r R
Tactic: use r
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (hypothesis)
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)
⊢ f R = c
have this : 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]