awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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 : ℤ
⊢ 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)
have 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)
Tactic: filter_upwards [h] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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
⊢ 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)
have 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)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIoc T a f) n = fourierCoeffOn (b := a + T) ⋯ f n
have 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))
Tactic: rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral, add_sub_cancel_left a T]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ 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))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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))
have 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)
Tactic: refine intervalIntegral.integral_congr_ae (ae_of_all _ fun x hx => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
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)
have e_a : x ∈ Ioc a (a + T)
Tactic: rw [liftIoc_coe_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ uIoc a (a + T)
⊢ x ∈ Ioc a (a + T)
have e_a : ∀ (hx : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIco T a f) n = fourierCoeffOn (b := a + T) ⋯ f n
have 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))
Tactic: rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral _ _ a, add_sub_cancel_left a T]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ 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))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
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) : ℂ)
        (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))
have 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))
Tactic: simp_rw [intervalIntegral.integral_of_le (lt_add_of_pos_right a hT.out).le]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ 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))
have 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))
Tactic: rw [integral_Ioc_eq_integral_Ioo]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ 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))
have 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))
Tactic: rw [integral_Ioc_eq_integral_Ioo]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ 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))
have 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))
Tactic: iterate 2 rw [integral_Ioc_eq_integral_Ioo]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ 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))
have e_a : ∀ (x : ℝ) (hx : x ∈ Ioo a (a + T)),
  HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
      (liftIco T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)) =
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x)
Tactic: refine setIntegral_congr_fun measurableSet_Ioo fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ Ioo a (a + T)
⊢ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
      (liftIco T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)) =
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x)
have e_a : HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x) =
  HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x)
Tactic: rw [liftIco_coe_apply (Ioo_subset_Ico_self hx)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ (↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
        (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
      i =
    fourierCoeff (↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) i
have trans : Eq (α := (fun (x : ℤ) ↦ ℂ) i)
  ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
      (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
    i)
  (∫ (t : AddCircle T),
    HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle)
Tactic: trans ∫ t : AddCircle T, conj ((@fourierLp T hT 2 _ i : AddCircle T → ℂ) t) * f t ∂haarAddCircle
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
trans :
  Eq (α := (fun (x : ℤ) ↦ ℂ) i)
    ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
        (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
      i)
    (∫ (t : AddCircle T),
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle)
⊢ (↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
        (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
      i =
    fourierCoeff (↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) i
have trans₁ : ∫ (t : AddCircle T),
    HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle =
  fourierCoeff (↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) i
Tactic: trans ∫ t : AddCircle T, conj ((@fourierLp T hT 2 _ i : AddCircle T → ℂ) t) * f t ∂haarAddCircle
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ Eq (α := (fun (x : ℤ) ↦ ℂ) i)
    ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
        (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
      i)
    (∫ (t : AddCircle T),
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle)
have rw : Eq (α := (fun (x : ℤ) ↦ ℂ) i)
  (∫ (a : AddCircle T),
    inner ℂ ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) ∂haarAddCircle)
  (∫ (t : AddCircle T),
    HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle)
Tactic: rw [fourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_fourierBasis]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ∫ (t : AddCircle T),
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle =
    fourierCoeff (↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) i
have h : (ae (F := Measure (AddCircle T)) haarAddCircle).EventuallyEq (β := (fun (x : ℤ) ↦ ℂ) i)
  (fun (a : AddCircle T) ↦
    HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a))
  fun (a : AddCircle T) ↦
  HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
    ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ (ae (F := Measure (AddCircle T)) haarAddCircle).EventuallyEq (β := (fun (x : ℤ) ↦ ℂ) i)
    (fun (a : AddCircle T) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a))
    fun (a : AddCircle T) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
have h : ∀ (a : AddCircle T)
  (ht :
    (↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a =
      (fourier i : (a : AddCircle T) → ℂ) a),
  HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
Tactic: filter_upwards [coeFn_fourierLp 2 i] with _ ht
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
a : AddCircle T
ht : (↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a = (fourier i : (a : AddCircle T) → ℂ) a
⊢ HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
have h : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier i : (a : AddCircle T) → ℂ) a : ℂ) : ℂ)
    ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
  HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
    ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
Tactic: rw [ht, ← fourier_neg, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
a : AddCircle T
ht : (↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a = (fourier i : (a : AddCircle T) → ℂ) a
h :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier i : (a : AddCircle T) → ℂ) a : ℂ) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
⊢ HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
have h₁ : HMul.hMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
    ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
  HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
    ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
Tactic: rw [ht, ← fourier_neg, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
a : AddCircle T
ht : (↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a = (fourier i : (a : AddCircle T) → ℂ) a
h :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier i : (a : AddCircle T) → ℂ) a : ℂ) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
h₁ :
  HMul.hMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
⊢ HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
have h₂ : HMul.hMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
    ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
  HMul.hMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
    ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
Tactic: rw [ht, ← fourier_neg, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum
    (fun (i : ℤ) ↦
      HSMul.hSMul (β := ↥(Lp ℂ 2 haarAddCircle))
        (fourierCoeff (↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) i) (fourierLp 2 i))
    f
have simp_rw : HasSum
  (fun (i : ℤ) ↦
    HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
      ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) : (i : ℤ) → ℂ)
        i)
      (fourierLp 2 i))
  f
Tactic: simp_rw [← fourierBasis_repr]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
        ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
            (i : ℤ) → ℂ)
          i)
        (fourierLp 2 i))
    f
have rw : HasSum
  (fun (i : ℤ) ↦
    HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
      ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) : (i : ℤ) → ℂ)
        i)
      ((fourierBasis : (a : ℤ) → ↥(Lp ℂ 2 haarAddCircle)) i : ↥(Lp ℂ 2 haarAddCircle)))
  f
Tactic: rw [← coe_fourierBasis]