awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
rw :
  HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)))) =
    HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x))
⊢ fourierCoeffOn hab f n =
    HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x))

Tactic:
rw [fourierCoeffOn, fourierCoeff_eq_intervalIntegral _ _ a, add_sub, add_sub_cancel_left]

Premises used: add_sub_cancel_left, add_sub, fourierCoeff_eq_intervalIntegral, fourierCoeffOn
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
e_a :
  Eq.{u_1 + 1} (α := E)
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))))
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
⊢ HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)))) =
    HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x))

Tactic:
congr 1
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
e_a :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
⊢ Eq.{u_1 + 1} (α := E)
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))))
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))

Tactic:
simp_rw [intervalIntegral.integral_of_le hab.le]

Premises used: LT.lt.le, intervalIntegral.integral_of_le
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))

Tactic:
setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
e_a :
  ∀ (x : ℝ) (hx : x ∈ Ioc a b),
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))) =
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
e_a : x ∈ Ioc a (a + (b - a))
⊢ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (liftIoc (b - a) a f (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a))) =
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (f x)

Tactic:
rw [liftIoc_coe_apply]

Premises used: AddCircle.liftIoc_coe_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
e_a : x ∈ Ioc a (a + b - a)
e_a₁ e_a₂ e_a₃ e_a₄ : x ∈ Ioc a b
⊢ x ∈ Ioc a (a + (b - a))

Tactic:
rwa [add_sub, add_sub_cancel_left]

Premises used: add_sub_cancel_left, add_sub
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
⊢ 0 < b - a

Tactic:
linarith
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
⊢ Fact (0 < b - a)

Tactic:
haveI := Fact.mk (by linarith : 0 < b - a)
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n

Tactic:
apply fourierCoeff.const_smul

Premises used: fourierCoeff.const_smul
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
a b : ℝ
f : ℝ → ℂ
c : ℂ
n : ℤ
hab : a < b
⊢ fourierCoeffOn hab (fun (x : ℝ) ↦ c * f x) n = c * fourierCoeffOn hab f n

Tactic:
fourierCoeffOn.const_smul _ _ _ _

Premises used: fourierCoeffOn.const_smul
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
h₁ : ∀ (n : ℤ), fourierCoeffOn hab f n = fourierCoeffOn hab g n
⊢ fourierCoeffOn hab f = fourierCoeffOn hab g

Tactic:
ext n
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
n : ℤ
h₁ :
  HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x)) =
    HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (g x))
⊢ fourierCoeffOn hab f n = fourierCoeffOn hab g n

Tactic:
rw [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]

Premises used: fourierCoeffOn_eq_integral
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
n : ℤ
h₁ :
  Eq.{u_1 + 1} (α := E)
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (g x))
⊢ HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x)) =
    HSMul.hSMul (β := E) (1 / (b - a))
      (∫ (x : ℝ) in a..b,
        HSMul.hSMul (α := ℂ)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (g x))

Tactic:
congr! 1
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
n : ℤ
h₁ :
  Filter.EventuallyEq.{0, u_1} (β := E) (ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b)))
    (fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
    fun (x : ℝ) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (g x)
⊢ Eq.{u_1 + 1} (α := E)
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
    (∫ (x : ℝ) in a..b,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (g x))

Tactic:
apply intervalIntegral.integral_congr_ae_restrict

Premises used: intervalIntegral.integral_congr_ae_restrict
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
n : ℤ
h₁ :
  Filter.EventuallyEq.{0, u_1} (β := E) (ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b)))
    (fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
    fun (x : ℝ) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (g x)
⊢ Filter.EventuallyEq.{0, u_1} (β := E) (ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b)))
    (fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
    fun (x : ℝ) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (g x)

Tactic:
simp only [uIoc_of_le hab.le]

Premises used: LT.lt.le, Set.uIoc_of_le
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
n : ℤ
h₁ :
  ∀ (x : ℝ) (hx : f x = g x),
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x) =
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (g x)
⊢ Filter.EventuallyEq.{0, u_1} (β := E) (ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b)))
    (fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x))
    fun (x : ℝ) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (g x)

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
n : ℤ
x : ℝ
hx : f x = g x
h₁ h₂ :
  HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (g x) =
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (g x)
⊢ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (f x) =
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (g x)

Tactic:
rw [hx]
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
rw :
  HSMul.hSMul (β := ℂ) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
          (liftIoc T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T))) =
    HSMul.hSMul (β := ℂ) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))
a₁ : ℝ
⊢ fourierCoeff (liftIoc T a f) n = fourierCoeffOn (b := a + T) ⋯ f n

Tactic:
rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral, add_sub_cancel_left a T]

Premises used: add_sub_cancel_left, fourierCoeff_eq_intervalIntegral, fourierCoeffOn_eq_integral
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
e_a :
  Eq (α := ℂ)
    (∫ (x : ℝ) in a..a + T,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIoc T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)))
    (∫ (x : ℝ) in a..a + T,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))
⊢ HSMul.hSMul (β := ℂ) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
          (liftIoc T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T))) =
    HSMul.hSMul (β := ℂ) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))

Tactic:
congr 1
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in a..a + T,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIoc T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)))
    (∫ (x : ℝ) in a..a + T,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))

Tactic:
intervalIntegral.integral_congr_ae (ae_of_all _ fun x hx => ?_)

Premises used: MeasureTheory.ae_of_all, intervalIntegral.integral_congr_ae
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
e_a :
  ∀ (x : ℝ) (hx : x ∈ uIoc a (a + T)),
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIoc T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)) =
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x)
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in a..a + T,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIoc T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)))
    (∫ (x : ℝ) in a..a + T,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))

Tactic:
refine intervalIntegral.integral_congr_ae (ae_of_all _ fun x hx => ?_)

Premises used: MeasureTheory.ae_of_all, intervalIntegral.integral_congr_ae
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ uIoc a (a + T)
e_a : x ∈ Ioc a (a + T)
⊢ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
      (liftIoc T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)) =
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x)

Tactic:
rw [liftIoc_coe_apply]

Premises used: AddCircle.liftIoc_coe_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ uIoc a (a + T)
e_a e_a₁ e_a₂ e_a₃ : ∀ (hx : x ∈ Ioc a (a + T)), x ∈ Ioc a (a + T)
⊢ x ∈ Ioc a (a + T)

Tactic:
rwa [uIoc_of_le (lt_add_of_pos_right a hT.out).le] at hx

Premises used: lt_add_of_pos_right, LT.lt.le, Set.uIoc_of_le, Fact.out
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
rw :
  HSMul.hSMul (β := ℂ) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
          (liftIco T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T))) =
    HSMul.hSMul (β := ℂ) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))
⊢ fourierCoeff (liftIco T a f) n = fourierCoeffOn (b := a + T) ⋯ f n

Tactic:
rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral _ _ a, add_sub_cancel_left a T]

Premises used: add_sub_cancel_left, fourierCoeff_eq_intervalIntegral, fourierCoeffOn_eq_integral
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
e_a :
  Eq (α := ℂ)
    (∫ (x : ℝ) in a..a + T,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)))
    (∫ (x : ℝ) in a..a + T,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))
⊢ HSMul.hSMul (β := ℂ) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
          (liftIco T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T))) =
    HSMul.hSMul (β := ℂ) (1 / T)
      (∫ (x : ℝ) in a..a + T,
        HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))

Tactic:
congr 1
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
e_a :
  Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a (a + T))) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a (a + T))) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in a..a + T,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)))
    (∫ (x : ℝ) in a..a + T,
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))

Tactic:
simp_rw [intervalIntegral.integral_of_le (lt_add_of_pos_right a hT.out).le]

Premises used: lt_add_of_pos_right, LT.lt.le, intervalIntegral.integral_of_le, Fact.out
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
e_a :
  Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioo a (a + T))) fun (t : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑t : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑t : ℝ ⧸ AddSubgroup.zmultiples T)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a (a + T))) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a (a + T))) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a (a + T))) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))

Tactic:
rw [integral_Ioc_eq_integral_Ioo]

Premises used: MeasureTheory.integral_Ioc_eq_integral_Ioo
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
e_a :
  Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioo a (a + T))) fun (t : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑t : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑t : ℝ ⧸ AddSubgroup.zmultiples T)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioo a (a + T))) fun (t : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑t : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f t))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioo a (a + T))) fun (t : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑t : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑t : ℝ ⧸ AddSubgroup.zmultiples T)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a (a + T))) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))

Tactic:
rw [integral_Ioc_eq_integral_Ioo]

Premises used: MeasureTheory.integral_Ioc_eq_integral_Ioo
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
e_a :
  Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioo a (a + T))) fun (t : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑t : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑t : ℝ ⧸ AddSubgroup.zmultiples T)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioo a (a + T))) fun (t : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑t : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f t))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a (a + T))) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a (a + T))) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x))

Tactic:
iterate 2 rw [integral_Ioc_eq_integral_Ioo]

Premises used: MeasureTheory.integral_Ioc_eq_integral_Ioo