awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
refine :
  HasDerivAt (fun (y : ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)) (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
    (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)))
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ)) * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))) (↑x : ℂ)

Tactic:
refine (hasDerivAt_exp _).comp (x : ℂ) ?_

Premises used: HasDerivAt.comp, Complex.ofReal, Complex.hasDerivAt_exp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun (x : ℂ) ↦ x * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))) (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
    (↑x : ℂ)

Tactic:
hasDerivAt_mul_const (2 * ↑π * I * ↑n / T)

Premises used: HMul.hMul, HDiv.hDiv, Complex.ofReal, hasDerivAt_mul_const, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
h :
  Eq (α := ℂ → ℂ) (fun (y : ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)) fun (x : ℂ) ↦
    x * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
⊢ HasDerivAt (fun (y : ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)) (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
    (↑x : ℂ)

Tactic:
convert! hasDerivAt_mul_const (2 * ↑π * I * ↑n / T) using 1

Premises used: HMul.hMul, HDiv.hDiv, Complex.ofReal, hasDerivAt_mul_const, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
h : ∀ (y : ℂ), 2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ) = y * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
⊢ Eq (α := ℂ → ℂ) (fun (y : ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)) fun (x : ℂ) ↦
    x * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))

Tactic:
ext1 y
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
y : ℂ
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ) = y * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.AddCircle
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

Tactic:
simpa using hasDerivAt_fourier T (-n) x

Premises used: hasDerivAt_fourier, Neg.neg
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ HasDerivAt
    (fun (x : ℝ) ↦
      HDiv.hDiv (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (-2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ)))
    (HMul.hMul (β := ℂ) (-2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
        ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) /
      (-2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ)))
    x

Tactic:
(hasDerivAt_fourier_neg T n x).div_const (-2 * π * I * n / T)

Premises used: Int.cast, Real.pi, HMul.hMul, HDiv.hDiv, hasDerivAt_fourier_neg, Complex.ofReal, HasDerivAt.div_const, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 : ℂ))
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 : ℂ))
⊢ 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

Tactic:
convert! (hasDerivAt_fourier_neg T n x).div_const (-2 * π * I * n / T) using 1

Premises used: Int.cast, Real.pi, HMul.hMul, HDiv.hDiv, hasDerivAt_fourier_neg, Complex.ofReal, HasDerivAt.div_const, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
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 : ℂ))
⊢ 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:
ext1 y
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x y : ℝ
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 : ℂ))
⊢ 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:
rw [div_div_eq_mul_div]

Premises used: div_div_eq_mul_div
-- Module: Mathlib.Analysis.Fourier.AddCircle
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) : ℂ) =
    HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (↑T : ℂ) /
      (-2 * (↑π : ℂ) * I * (↑n : ℂ))

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (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:
simp [mul_div_cancel_left₀, hn, (Fact.out : 0 < T).ne', Real.pi_pos.ne']

Premises used: mul_div_cancel_left₀, Real.pi_pos, LT.lt.ne', Fact.out
-- Module: Mathlib.Analysis.Fourier.AddCircle
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
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)
⊢ 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]

Premises used: Complex.ofReal_sub
-- Module: Mathlib.Analysis.Fourier.AddCircle
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
linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
⊢ 0 < b - a

Tactic:
linarith
-- Module: Mathlib.Analysis.Fourier.AddCircle
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
⊢ Fact (0 < b - a)

Tactic:
have hT : Fact (0 < b - a) := ⟨by linarith⟩
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
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)))
⊢ 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:
simp_rw [fourierCoeffOn_eq_integral, smul_eq_mul, real_smul, ofReal_div, ofReal_one]

Premises used: Complex.real_smul, Complex.ofReal_one, Complex.ofReal_div, fourierCoeffOn_eq_integral, smul_eq_mul
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
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)))

Tactic:
pattern (occs := 1 2 3) fourier _ _ * _

Premises used: fourier, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 : ℝ
rw :
  HMul.hMul (β := ℂ) (f x) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 : ℝ
this :
  HMul.hMul (β := ℂ) (f x) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f x)

Tactic:
(rw [mul_comm])

Premises used: mul_comm
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
rw :
  HMul.hMul (β := ℂ) (f b - f a)
    ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
    (f b - f a)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
this :
  HMul.hMul (β := ℂ) (f b - f a)
    ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
    (f b - f a)

Tactic:
(rw [mul_comm])

Premises used: mul_comm
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 : ℝ
rw :
  HMul.hMul (β := ℂ) (f' x) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f' x)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 : ℝ
this :
  HMul.hMul (β := ℂ) (f' x) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
| HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) (f' x)

Tactic:
(rw [mul_comm])

Premises used: mul_comm
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 (β := ℂ) (f x)
      ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
pattern₁ :
  HMul.hMul (β := ℂ) (f b - f a)
    ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
pattern₂ :
  ∀ (x : ℝ),
    HMul.hMul (β := ℂ) (f' x)
      ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (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)))

Tactic:
pattern (occs := 1 2 3) fourier _ _ * _ <;> (rw [mul_comm])

Premises used: fourier, mul_comm, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
conv :
  1 / (↑(b - a) : ℂ) *
      ∫ (x : ℝ) in a..b,
        HMul.hMul (β := ℂ) (f x)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (β := ℂ) (f b - f a)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) -
        (↑(b - a) : ℂ) *
          (1 / (↑(b - a) : ℂ) *
            ∫ (x : ℝ) in a..b,
              HMul.hMul (β := ℂ) (f' x)
                ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (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)))

Tactic:
conv => pattern (occs := 1 2 3) fourier _ _ * _ <;> (rw [mul_comm])

Premises used: fourier, mul_comm, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
rw :
  1 / (↑(b - a) : ℂ) *
      (f b *
            HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
              ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) -
          f a *
            HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
              ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) -
        ∫ (x : ℝ) in a..b,
          f' x *
            HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
              ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (β := ℂ) (f b - f a)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) -
        (↑(b - a) : ℂ) *
          (1 / (↑(b - a) : ℂ) *
            ∫ (x : ℝ) in a..b,
              HMul.hMul (β := ℂ) (f' x)
                ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)))
⊢ 1 / (↑(b - a) : ℂ) *
      ∫ (x : ℝ) in a..b,
        HMul.hMul (β := ℂ) (f x)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (β := ℂ) (f b - f a)
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) -
        (↑(b - a) : ℂ) *
          (1 / (↑(b - a) : ℂ) *
            ∫ (x : ℝ) in a..b,
              HMul.hMul (β := ℂ) (f' x)
                ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)))

Tactic:
rw [integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right hf
    (fun x _ ↦ has_antideriv_at_fourier_neg hT hn x |>.continuousAt |>.continuousWithinAt) hff'
    (fun x _ ↦ has_antideriv_at_fourier_neg hT hn x |>.hasDerivWithinAt) hf'
    (((map_continuous (fourier (-n))).comp (AddCircle.continuous_mk' _)).intervalIntegrable _ _)]

Premises used: HasDerivAt.hasDerivWithinAt, Continuous.comp, ContinuousAt.continuousWithinAt, intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right, has_antideriv_at_fourier_neg, fourier, Continuous.intervalIntegrable, HasDerivAt.continuousAt, AddCircle.continuous_mk', ContinuousMapClass.map_continuous, Neg.neg
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
u v w : ℂ
⊢ u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
⊢ ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)

Tactic:
have : ∀ u v w : ℂ, u * ((b - a : ℝ) / v * w) = (b - a : ℝ) / v * (u * w) := by intros; ring
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
f₁ :
  fun (x : ℝ) ↦
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
a₁ : a
b₁ : b
μ : volume
| ∫ (x : ℝ) in a..b,
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)

Tactic:
congr
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
f₁ :
  ∀ (x : ℝ),
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
| fun (x : ℝ) ↦
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)

Tactic:
ext
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
x : ℝ
f₁ :
  (↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
    HMul.hMul (β := ℂ) (f' x)
      ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
| f' x *
    HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
      ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
f₁ :
  ∀ (x : ℝ),
    (↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      HMul.hMul (β := ℂ) (f' x)
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
a₁ : a
b₁ : b
μ : volume
| ∫ (x : ℝ) in a..b,
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)

Tactic:
congr; ext; rw [this]