awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
this : Tendsto f (𝓝[<] R) (𝓝 (f R))
apply : (fun (x : ℝ) ↦ c) =ᶠ[𝓝[<] R] f
⊢ f R = c

Tactic:
apply tendsto_nhds_unique this (tendsto_const_nhds.congr' _)

Premises used: tendsto_const_nhds, Filter.Tendsto.congr', tendsto_nhds_unique
-- 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)
this : Tendsto f (𝓝[<] R) (𝓝 (f R))
⊢ (fun (x : ℝ) ↦ c) =ᶠ[𝓝[<] R] f

Tactic:
apply Filter.eventuallyEq_of_mem (Ioo_mem_nhdsLT hR) (fun _ hx ↦ (h₂f hx).symm)

Premises used: Filter.eventuallyEq_of_mem, Ioo_mem_nhdsLT, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
a : E
c : ℂ
R : ℝ
simp : ((2 * π)⁻¹ * (2 * π)) • a = a
⊢ circleAverage (fun (x : ℂ) ↦ a) c R = a

Tactic:
simp only [circleAverage, intervalIntegral.integral_const, ← smul_assoc, sub_zero, smul_eq_mul]

Premises used: smul_assoc, sub_zero, smul_eq_mul, intervalIntegral.integral_const, Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
a : E
c : ℂ
R : ℝ
ring_nf : (π * π⁻¹) • a = a
⊢ ((2 * π)⁻¹ * (2 * π)) • a = a

Tactic:
ring_nf
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
a : E
c : ℂ
R : ℝ
⊢ (π * π⁻¹) • a = a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
rw : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) = a
⊢ circleAverage f c R = a

Tactic:
rw [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 : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
left : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
| HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) = a

Tactic:
left
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
arg : ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)
| HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))

Tactic:
arg 2
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
arg : fun (θ : ℝ) ↦ f (circleMap c R θ)
| ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)

Tactic:
arg 1
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
θ : ℝ
h : a
| f (circleMap c R θ)

Tactic:
rw [hf (circleMap c R θ) (circleMap_mem_sphere' c R θ)]

Premises used: circleMap, circleMap_mem_sphere'
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
h : ∀ (θ : ℝ), a
| HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) = a

Tactic:
left; arg 2; arg 1
    intro θ
    rw [hf (circleMap c R θ) (circleMap_mem_sphere' c R θ)]
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
conv : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, a) = a
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) = a

Tactic:
conv =>
    left; arg 2; arg 1
    intro θ
    rw [hf (circleMap c R θ) (circleMap_mem_sphere' c R θ)]
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, a) = a

Tactic:
apply circleAverage_const a c R

Premises used: Real.circleAverage_const
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
⊢ 0 < (2 * π)⁻¹

Tactic:
simp [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
apply : LE.le (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
⊢ circleAverage f₁ c R ≤ circleAverage f₂ c R

Tactic:
apply (mul_le_mul_iff_of_pos_left (by simp [pi_pos])).2

Premises used: Iff.mpr, mul_le_mul_iff_of_pos_left
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
apply : ∀ x ∈ Ioo 0 (2 * π), f₁ (circleMap c R x) ≤ f₂ (circleMap c R x)
⊢ LE.le (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))

Tactic:
apply intervalIntegral.integral_mono_on_of_le_Ioo (le_of_lt two_pi_pos) hf₁ hf₂

Premises used: intervalIntegral.integral_mono_on_of_le_Ioo, le_of_lt, Real.two_pi_pos
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
x : ℝ
h_1 : x ∈ Ioo 0 (2 * π)
⊢ f₁ (circleMap c R x) ≤ f₂ (circleMap c R x)

Tactic:
simp [h (circleMap c R x)]

Premises used: circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
⊢ ∀ x ∈ Ioo 0 (2 * π), f₁ (circleMap c R x) ≤ f₂ (circleMap c R x)

Tactic:
exact fun x _ ↦ by simp [h (circleMap c R x)]
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
rw : LE.le (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, a)
⊢ circleAverage f c R ≤ a

Tactic:
rw [← circleAverage_const a c |R|, circleAverage, circleAverage, smul_eq_mul, smul_eq_mul,
    mul_le_mul_iff_of_pos_left (inv_pos.2 two_pi_pos)]

Premises used: Iff.mpr, abs, mul_le_mul_iff_of_pos_left, inv_pos, Real.two_pi_pos, smul_eq_mul, Real.circleAverage_const, Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ LE.le (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, a)

Tactic:
intervalIntegral.integral_mono_on_of_le_Ioo (le_of_lt two_pi_pos) hf
    intervalIntegrable_const (fun θ _ ↦ h₂f (circleMap c R θ) (circleMap_mem_sphere' c R θ))

Premises used: intervalIntegral.integral_mono_on_of_le_Ioo, le_of_lt, circleMap, Real.two_pi_pos, intervalIntegrable_const, circleMap_mem_sphere'
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ LE.le (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, a)

Tactic:
exact intervalIntegral.integral_mono_on_of_le_Ioo (le_of_lt two_pi_pos) hf
    intervalIntegrable_const (fun θ _ ↦ h₂f (circleMap c R θ) (circleMap_mem_sphere' c R θ))

Premises used: intervalIntegral.integral_mono_on_of_le_Ioo, le_of_lt, circleMap, Real.two_pi_pos, intervalIntegrable_const, circleMap_mem_sphere'
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
rw : LE.le (α := ℝ) |∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)| (∫ (θ : ℝ) in 0..2 * π, |f| (circleMap c R θ))
⊢ |circleAverage f c R| ≤ circleAverage |f| c R

Tactic:
rw [circleAverage, circleAverage, smul_eq_mul, smul_eq_mul, abs_mul,
    abs_of_pos (inv_pos.2 two_pi_pos), mul_le_mul_iff_of_pos_left (inv_pos.2 two_pi_pos)]

Premises used: Iff.mpr, abs_mul, mul_le_mul_iff_of_pos_left, inv_pos, Real.two_pi_pos, abs_of_pos, smul_eq_mul, Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
⊢ LE.le (α := ℝ) |∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)| (∫ (θ : ℝ) in 0..2 * π, |f| (circleMap c R θ))

Tactic:
intervalIntegral.abs_integral_le_integral_abs (le_of_lt two_pi_pos)

Premises used: abs, le_of_lt, Real.two_pi_pos, intervalIntegral.abs_integral_le_integral_abs
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
⊢ LE.le (α := ℝ) |∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)| (∫ (θ : ℝ) in 0..2 * π, |f| (circleMap c R θ))

Tactic:
exact intervalIntegral.abs_integral_le_integral_abs (le_of_lt two_pi_pos)

Premises used: le_of_lt, Real.two_pi_pos, intervalIntegral.abs_integral_le_integral_abs
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
pos : ∀ (hf : CircleIntegrable f c R), 0 ≤ circleAverage f c R
neg : ∀ (hf : ¬CircleIntegrable f c R), 0 ≤ circleAverage f c R
⊢ 0 ≤ circleAverage f c R

Tactic:
by_cases hf : CircleIntegrable f c R

Premises used: CircleIntegrable
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
hf : CircleIntegrable f c R
pos : LE.le (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, 0) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
⊢ 0 ≤ circleAverage f c R

Tactic:
rw [← circleAverage_const 0 c |R|, circleAverage, circleAverage, smul_eq_mul, smul_eq_mul,
      mul_le_mul_iff_of_pos_left (inv_pos.2 two_pi_pos)]

Premises used: Iff.mpr, abs, mul_le_mul_iff_of_pos_left, inv_pos, Real.two_pi_pos, smul_eq_mul, OfNat.ofNat, Real.circleAverage_const, Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
hf : CircleIntegrable f c R
⊢ LE.le (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, 0) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))

Tactic:
apply intervalIntegral.integral_mono_on_of_le_Ioo (le_of_lt two_pi_pos)
      intervalIntegrable_const hf (fun θ _ ↦ h₂f (circleMap c R θ) (circleMap_mem_sphere' c R θ))

Premises used: intervalIntegral.integral_mono_on_of_le_Ioo, le_of_lt, circleMap, Real.two_pi_pos, intervalIntegrable_const, circleMap_mem_sphere'
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
hf : ¬CircleIntegrable f c R
neg neg₁ : LE.le (α := ℝ) 0 0
⊢ 0 ≤ circleAverage f c R

Tactic:
rw [circleAverage.integral_undef hf]

Premises used: Real.circleAverage.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
c : ℂ
R : ℝ
inst_5 : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
unfold :
  HSMul.hSMul (β := F) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ)) =
    (L : (a : E) → F) (HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)))
⊢ Eq.{u_2 + 1} (α := F) (circleAverage ((⇑L : (a : E) → F) ∘ f) c R : F) ((L : (a : E) → F) (circleAverage f c R) : F)

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 : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
c : ℂ
R : ℝ
inst_5 : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
rw :
  HSMul.hSMul (β := F) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ)) =
    HSMul.hSMul (β := F) (2 * π)⁻¹ ((L : (a : E) → F) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) : F)
⊢ HSMul.hSMul (β := F) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ)) =
    (L : (a : E) → F) (HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)))

Tactic:
rw [map_smul]

Premises used: map_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
c : ℂ
R : ℝ
inst_5 : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
e_a :
  Eq.{u_2 + 1} (α := F) (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ) : F)
    ((L : (a : E) → F) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) : F)
⊢ HSMul.hSMul (β := F) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ)) =
    HSMul.hSMul (β := F) (2 * π)⁻¹ ((L : (a : E) → F) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) : F)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
c : ℂ
R : ℝ
inst_5 : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
⊢ Eq.{u_2 + 1} (α := F) (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ) : F)
    ((L : (a : E) → F) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) : F)

Tactic:
L.intervalIntegral_comp_comm hf

Premises used: ContinuousLinearMap.intervalIntegral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
c : ℂ
R : ℝ
inst_5 : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
⊢ Eq.{u_2 + 1} (α := F) (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ) : F)
    ((L : (a : E) → F) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) : F)

Tactic:
exact L.intervalIntegral_comp_comm hf

Premises used: ContinuousLinearMap.intervalIntegral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NormedDivisionRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : NormSMulClass 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
f : ℂ → E
c : ℂ
R : ℝ
a : 𝕜
unfold :
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (a • f) (circleMap c R θ)) =
    a • HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
⊢ circleAverage (a • f) c R = a • 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
𝕜 : Type u_3
inst_2 : NormedDivisionRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : NormSMulClass 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
f : ℂ → E
c : ℂ
R : ℝ
a : 𝕜
⊢ SMulCommClass 𝕜 ℝ E

Tactic:
have := SMulCommClass.symm ℝ 𝕜 E
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NormedDivisionRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : NormSMulClass 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
f : ℂ → E
c : ℂ
R : ℝ
a : 𝕜
this : SMulCommClass 𝕜 ℝ E
rw :
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (a • f) (circleMap c R θ)) =
    (2 * π)⁻¹ • HSMul.hSMul (β := E) a (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (a • f) (circleMap c R θ)) =
    a • HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))

Tactic:
rw [smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NormedDivisionRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : NormSMulClass 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
f : ℂ → E
c : ℂ
R : ℝ
a : 𝕜
this : SMulCommClass 𝕜 ℝ E
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (a • f) (circleMap c R θ)) =
    (2 * π)⁻¹ • HSMul.hSMul (β := E) a (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))

Tactic:
simp [intervalIntegral.integral_smul]

Premises used: intervalIntegral.integral_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NormedDivisionRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : NormSMulClass 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
f : ℂ → E
c : ℂ
R : ℝ
a : 𝕜
⊢ circleAverage (fun (z : ℂ) ↦ a • f z) c R = a • circleAverage f c R

Tactic:
circleAverage_smul

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

Tactic:
rw [circleAverage, circleAverage, circleAverage, ← smul_add]

Premises used: smul_add, 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₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
e_a :
  ∫ (θ : ℝ) in 0..2 * π, (f₁ + f₂) (circleMap c R θ) =
    HAdd.hAdd (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (f₁ + f₂) (circleMap c R θ)) =
    (2 * π)⁻¹ •
      HAdd.hAdd (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..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₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ ∫ (θ : ℝ) in 0..2 * π, (f₁ + f₂) (circleMap c R θ) =
    HAdd.hAdd (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))

Tactic:
apply intervalIntegral.integral_add hf₁ hf₂

Premises used: intervalIntegral.integral_add
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ circleAverage (fun (z : ℂ) ↦ f₁ z + f₂ z) c R = circleAverage f₁ c R + circleAverage f₂ c R

Tactic:
circleAverage_add hf₁ hf₂

Premises used: Real.circleAverage_add
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
unfold :
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (∑ i ∈ s, f i) (circleMap c R θ)) =
    ∑ i ∈ s, HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f i (circleMap c R θ))
⊢ Eq.{u_1 + 1} (α := E) (circleAverage (∑ i ∈ s, f i) c R) (∑ i ∈ s, circleAverage (f i) 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 : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (∑ i ∈ s, f i) (circleMap c R θ)) =
    ∑ i ∈ s, HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f i (circleMap c R θ))

Tactic:
simp [← Finset.smul_sum, intervalIntegral.integral_finsetSum h]

Premises used: intervalIntegral.integral_finsetSum, Finset.smul_sum
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ Eq.{u_1 + 1} (α := E) (circleAverage (∑ i ∈ s, f i) c R) (∑ i ∈ s, circleAverage (f i) c R)

Tactic:
circleAverage_sum h

Premises used: Real.circleAverage_sum
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
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)
⊢ Eq.{u_1 + 1} (α := E) (circleAverage (fun (z : ℂ) ↦ ∑ i ∈ s, f i z) c R) (∑ i ∈ s, circleAverage (f i) c R)

Tactic:
convert! circleAverage_sum h

Premises used: Real.circleAverage_sum
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
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.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
rw :
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ)) =
    (2 * π)⁻¹ •
      HSub.hSub (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
⊢ circleAverage (f₁ - f₂) c R = circleAverage f₁ c R - circleAverage f₂ c R

Tactic:
rw [circleAverage, circleAverage, circleAverage, ← smul_sub]

Premises used: smul_sub, 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₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
e_a :
  ∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ) =
    HSub.hSub (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ)) =
    (2 * π)⁻¹ •
      HSub.hSub (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..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₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ ∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ) =
    HSub.hSub (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))

Tactic:
apply intervalIntegral.integral_sub hf₁ hf₂

Premises used: intervalIntegral.integral_sub
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ circleAverage (fun (z : ℂ) ↦ f₁ z - f₂ z) c R = circleAverage f₁ c R - circleAverage f₂ c R

Tactic:
circleAverage_sub hf₁ hf₂

Premises used: Real.circleAverage_sub
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c : ℂ
R : ℝ
⊢ range (circleMap c R) = c +ᵥ HSMul.hSMul (β := Set ℂ) R (range fun (θ : ℝ) ↦ cexp ((↑θ : ℂ) * I))

Tactic:
simp +unfoldPartialApp only [← image_vadd, ← image_smul, ← range_comp,
        vadd_eq_add, circleMap, comp_def, real_smul]

Premises used: Set.range_comp, Complex.real_smul, Set.image_smul, circleMap, Set.image_vadd, Function.comp_def, vadd_eq_add