awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (α := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ))
⊢ HasSum
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := C(AddCircle T, ℂ)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) i) (fourier i))
    f
have sum_L2 : HasSum (α := ↥(Lp ℂ 2 haarAddCircle))
  (fun (i : ℤ) ↦
    HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
      (fourierCoeff (T := T)
        (↑(↑((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f) :
              AddCircle T →ₘ[haarAddCircle] ℂ) :
          AddCircle T → ℂ)
        i)
      (fourierLp 2 i))
  ((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f : ↥(Lp ℂ 2 haarAddCircle))
Tactic: have sum_L2 := hasSum_fourier_series_L2 (toLp (E := ℂ) 2 haarAddCircle ℂ f)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (α := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ))
sum_L2 :
  HasSum (α := ↥(Lp ℂ 2 haarAddCircle))
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
        (fourierCoeff (T := T)
          (↑(↑((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f) :
                AddCircle T →ₘ[haarAddCircle] ℂ) :
            AddCircle T → ℂ)
          i)
        (fourierLp 2 i))
    ((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f : ↥(Lp ℂ 2 haarAddCircle))
⊢ HasSum
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := C(AddCircle T, ℂ)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) i) (fourier i))
    f
have sum_L2₁ : HasSum (α := ↥(Lp ℂ 2 haarAddCircle))
  (fun (i : ℤ) ↦
    HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) i)
      (fourierLp 2 i))
  ((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f : ↥(Lp ℂ 2 haarAddCircle))
Tactic: simp_rw [fourierCoeff_toLp] at sum_L2
Cleared hypotheses: sum_L2
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (α := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ))
sum_L2 :
  HasSum (α := ↥(Lp ℂ 2 haarAddCircle))
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) i)
        (fourierLp 2 i))
    ((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f : ↥(Lp ℂ 2 haarAddCircle))
⊢ Summable (α := ℝ) fun (a : ℤ) ↦
    ‖HSMul.hSMul (α := ℂ) (β := C(AddCircle T, ℂ)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) a) (fourier a)‖
have simp_rw : Summable (α := ℝ) fun (a : ℤ) ↦ norm (E := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) a)
Tactic: simp_rw [norm_smul, fourier_norm, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
⊢ Eq (α := (n : ℤ) → ℂ) (fourierCoeff (T := T) (⇑(fourier n) : (a : AddCircle T) → ℂ))
    (Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1)
have h : ∀ (m : ℤ),
  Eq (α := ℂ) (fourierCoeff (T := T) (⇑(fourier n) : (a : AddCircle T) → ℂ) m : ℂ)
    (Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m : ℂ)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n m : ℤ
⊢ Eq (α := ℂ) (fourierCoeff (T := T) (⇑(fourier n) : (a : AddCircle T) → ℂ) m : ℂ)
    (Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m : ℂ)
have h : inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 n) = Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m
Tactic: rw [← fourierCoeff_congr_ae (coeFn_fourierLp 2 n), ← fourierBasis_repr,
    HilbertBasis.repr_apply_apply, coe_fourierBasis]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n m : ℤ
⊢ inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 n) = Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m
have h : inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 m) = Pi.single (M := fun (j : ℤ) ↦ ℂ) m 1 m
Tactic: obtain (rfl | hmn) := eq_or_ne m n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n m : ℤ
h : inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 m) = Pi.single (M := fun (j : ℤ) ↦ ℂ) m 1 m
⊢ inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 n) = Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m
have h₁ : ∀ (hmn : m ≠ n),
  inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 n) = Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m
Tactic: obtain (rfl | hmn) := eq_or_ne m n
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
m : ℤ
⊢ inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 m) = Pi.single (M := fun (j : ℤ) ↦ ℂ) m 1 m
have h : HPow.hPow (α := ℂ) (β := ℕ) (↑1 : ℂ) 2 = Pi.single (M := fun (j : ℤ) ↦ ℂ) m 1 m
Tactic: rw [inner_self_eq_norm_sq_to_K, (orthonormal_fourier (hT := hT)).1 m]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n m : ℤ
hmn : m ≠ n
⊢ inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 n) = Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m
have h : Eq (α := ℂ) (0 : ℂ) (Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m : ℂ)
Tactic: rw [(orthonormal_fourier (hT := hT)).2 hmn]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun (y : ℝ) ↦ (fourier n : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T))
    (HMul.hMul (β := ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
      ((fourier n : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ))
    x
have simp_rw : HasDerivAt (fun (y : ℝ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑y : ℂ) / (↑T : ℂ)))
  (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))) x
Tactic: simp_rw [fourier_coe_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun (y : ℝ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑y : ℂ) / (↑T : ℂ)))
    (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))) x
have refine : HasDerivAt (fun (y : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)))
  (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))) (↑x : ℂ)
Tactic: refine (?_ : HasDerivAt (fun y => exp (2 * π * I * n * y / T)) _ _).comp_ofReal
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun (y : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)))
    (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))) (↑x : ℂ)
have rw : HasDerivAt (fun (y : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)))
  (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ)) * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))) (↑x : ℂ)
Tactic: rw [(fun α β => by ring : ∀ α β : ℂ, α * exp β = exp β * α)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun (y : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)))
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ)) * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))) (↑x : ℂ)
have refine : HasDerivAt (fun (y : ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)) (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ)) (↑x : ℂ)
Tactic: refine (hasDerivAt_exp _).comp (x : ℂ) ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun (y : ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)) (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
    (↑x : ℂ)
have h : Eq (α := ℂ → ℂ) (fun (y : ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)) fun (x : ℂ) ↦
  x * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
Tactic: convert! hasDerivAt_mul_const (2 * ↑π * I * ↑n / T) using 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ Eq (α := ℂ → ℂ) (fun (y : ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)) fun (x : ℂ) ↦
    x * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
have h : ∀ (y : ℂ), 2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ) = y * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
Tactic: ext1 y
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ HasDerivAt (F := ℂ)
    (fun (y : ℝ) ↦
      HMul.hMul (β := ℂ) ((↑T : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ))
    ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) x
have h : Eq (α := ℝ → ℂ)
  (fun (y : ℝ) ↦
    HMul.hMul (β := ℂ) ((↑T : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
      ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ))
  fun (x : ℝ) ↦
  HDiv.hDiv (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
    (-2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
Tactic: convert! (hasDerivAt_fourier_neg T n x).div_const (-2 * π * I * n / T) using 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
h :
  Eq (α := ℝ → ℂ)
    (fun (y : ℝ) ↦
      HMul.hMul (β := ℂ) ((↑T : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ))
    fun (x : ℝ) ↦
    HDiv.hDiv (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
      (-2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
⊢ HasDerivAt (F := ℂ)
    (fun (y : ℝ) ↦
      HMul.hMul (β := ℂ) ((↑T : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ))
    ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) x
have h₁ : (fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) =
  HMul.hMul (β := ℂ) (-2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
      ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) /
    (-2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
Tactic: convert! (hasDerivAt_fourier_neg T n x).div_const (-2 * π * I * n / T) using 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ Eq (α := ℝ → ℂ)
    (fun (y : ℝ) ↦
      HMul.hMul (β := ℂ) ((↑T : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ))
    fun (x : ℝ) ↦
    HDiv.hDiv (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
      (-2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
have h : ∀ (y : ℝ),
  HMul.hMul (β := ℂ) ((↑T : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
      ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) =
    HDiv.hDiv (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
      (-2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
Tactic: ext1 y
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x y : ℝ
⊢ HMul.hMul (β := ℂ) ((↑T : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
      ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) =
    HDiv.hDiv (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
      (-2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
have h : HMul.hMul (β := ℂ) ((↑T : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
    ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) =
  HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (↑T : ℂ) /
    (-2 * (↑π : ℂ) * I * (↑n : ℂ))
Tactic: rw [div_div_eq_mul_div]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
⊢ fourierCoeffOn hab f n =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (f b - f a) -
        ((↑b : ℂ) - (↑a : ℂ)) * fourierCoeffOn hab f' n)
have rw : fourierCoeffOn hab f n =
  1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
    (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f b - f a) -
      (↑(b - a) : ℂ) * fourierCoeffOn hab f' n)
Tactic: rw [← ofReal_sub]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
⊢ 0 < b - a
have linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
⊢ fourierCoeffOn hab f n =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (f b - f a) -
        (↑(b - a) : ℂ) * fourierCoeffOn hab f' n)
have hT : Fact (0 < b - a)
Tactic: have hT : Fact (0 < b - a) := ⟨by linarith⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ fourierCoeffOn hab f n =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (f b - f a) -
        (↑(b - a) : ℂ) * fourierCoeffOn hab f' n)
have simp_rw : 1 / (↑(b - a) : ℂ) *
    ∫ (x : ℝ) in a..b,
      HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f x) =
  1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
    (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
        (f b - f a) -
      (↑(b - a) : ℂ) *
        (1 / (↑(b - a) : ℂ) *
          ∫ (x : ℝ) in a..b,
            HMul.hMul (α := ℂ)
              ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f' x)))
Tactic: simp_rw [fourierCoeffOn_eq_integral, smul_eq_mul, real_smul, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| 1 / (↑(b - a) : ℂ) *
      ∫ (x : ℝ) in a..b,
        HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (f x) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (f b - f a) -
        (↑(b - a) : ℂ) *
          (1 / (↑(b - a) : ℂ) *
            ∫ (x : ℝ) in a..b,
              HMul.hMul (α := ℂ)
                ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f' x)))
have pattern : ∀ (x : ℝ),
  HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x)
Tactic: pattern (occs := 1 2 3) fourier _ _ * _
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
pattern :
  ∀ (x : ℝ),
    HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (f x)
| 1 / (↑(b - a) : ℂ) *
      ∫ (x : ℝ) in a..b,
        HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (f x) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (f b - f a) -
        (↑(b - a) : ℂ) *
          (1 / (↑(b - a) : ℂ) *
            ∫ (x : ℝ) in a..b,
              HMul.hMul (α := ℂ)
                ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f' x)))
have pattern₁ : HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
  (f b - f a)
Tactic: pattern (occs := 1 2 3) fourier _ _ * _
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
pattern :
  ∀ (x : ℝ),
    HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
      (f x)
pattern₁ :
  HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
    (f b - f a)
| 1 / (↑(b - a) : ℂ) *
      ∫ (x : ℝ) in a..b,
        HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (f x) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (f b - f a) -
        (↑(b - a) : ℂ) *
          (1 / (↑(b - a) : ℂ) *
            ∫ (x : ℝ) in a..b,
              HMul.hMul (α := ℂ)
                ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f' x)))
have pattern₂ : ∀ (x : ℝ),
  HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f' x)
Tactic: pattern (occs := 1 2 3) fourier _ _ * _
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x)
have rw : HMul.hMul (β := ℂ) (f x) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x)
have this : HMul.hMul (β := ℂ) (f x) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: (rw [mul_comm])
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
    (f b - f a)
have rw : HMul.hMul (β := ℂ) (f b - f a)
  ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
    (f b - f a)
have this : HMul.hMul (β := ℂ) (f b - f a)
  ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: (rw [mul_comm])
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f' x)
have rw : HMul.hMul (β := ℂ) (f' x) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f' x)
have this : HMul.hMul (β := ℂ) (f' x) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: (rw [mul_comm])
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| 1 / (↑(b - a) : ℂ) *
      ∫ (x : ℝ) in a..b,
        HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (f x) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
          (f b - f a) -
        (↑(b - a) : ℂ) *
          (1 / (↑(b - a) : ℂ) *
            ∫ (x : ℝ) in a..b,
              HMul.hMul (α := ℂ)
                ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f' x)))
have pattern : ∀ (x : ℝ),
  HMul.hMul (β := ℂ) (f x) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: pattern (occs := 1 2 3) fourier _ _ * _ <;> (rw [mul_comm])