awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
conv :
  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,
          (↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
            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) : ℂ) *
      (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)) : ℂ)))

Tactic:
conv in intervalIntegral _ _ _ _ => congr; ext; rw [this]

Premises used: intervalIntegral
-- 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)
⊢ (↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) = (↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))

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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
rw :
  1 / (↑(b - a) : ℂ) *
      (f b *
            HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
              ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) -
          f a *
            HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
              ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) -
        ∫ (x : ℝ) in a..b,
          (↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))) *
            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) : ℂ) *
      (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,
          (↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
            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 [(by ring : ((b - a : ℝ) : ℂ) / (-2 * π * I * n) = ((b - a : ℝ) : ℂ) * (1 / (-2 * π * I * n)))]
-- 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)
⊢ Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (b - a)))
    (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a))

Tactic:
simpa using coe_add_period (b - a) a

Premises used: AddCircle.coe_add_period, HSub.hSub
-- 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)
⊢ Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (b - a)))
    (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a))

Tactic:
have s2 : (b : AddCircle (b - a)) = (a : AddCircle (b - a)) := by
    simpa using coe_add_period (b - a) a
-- 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)
s2 :
  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (b - a)))
    (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a))
rw :
  1 / (↑(b - a) : ℂ) *
        ((f b - f a) *
          HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
            ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)) -
      1 / (↑(b - a) : ℂ) *
        ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))) *
          ∫ (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)) : ℂ) -
      1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
        ((↑(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) : ℂ) *
      (f b *
            HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
              ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) -
          f a *
            HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
              ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) -
        ∫ (x : ℝ) in a..b,
          (↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))) *
            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 [s2, intervalIntegral.integral_const_mul, ← sub_mul, mul_sub, mul_sub]

Premises used: mul_sub, sub_mul, intervalIntegral.integral_const_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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
s2 :
  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (b - a)))
    (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a))
e_a :
  1 / (↑(b - a) : ℂ) *
      ((f b - f a) *
        HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ 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)) : ℂ)
e_a₁ :
  1 / (↑(b - a) : ℂ) *
      ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))) *
        ∫ (x : ℝ) in a..b,
          HMul.hMul (β := ℂ) (f' x)
            ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((↑(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) : ℂ) *
        ((f b - f a) *
          HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
            ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)) -
      1 / (↑(b - a) : ℂ) *
        ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))) *
          ∫ (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)) : ℂ) -
      1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
        ((↑(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:
congr 1
-- 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)
s2 :
  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (b - a)))
    (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a))
rw :
  (f b - f a) *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) /
    (↑(b - a) : ℂ)
| 1 / (↑(b - a) : ℂ) *
    ((f b - f a) *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ))

Tactic:
rw [mul_comm, mul_div, mul_one]

Premises used: mul_div, mul_comm, mul_one
-- 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)
s2 :
  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (b - a)))
    (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a))
e_a :
  (f b - f a) *
        HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) /
      (↑(b - a) : ℂ) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      HMul.hMul (β := ℂ) (f b - f a)
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
⊢ 1 / (↑(b - a) : ℂ) *
      ((f b - f a) *
        HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ 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)) : ℂ)

Tactic:
conv_lhs => rw [mul_comm, mul_div, mul_one]

Premises used: mul_div, mul_comm, mul_one
-- 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)
s2 :
  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (b - a)))
    (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a))
e_a :
  (f b - f a) *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ 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) : ℂ)
⊢ (f b - f a) *
        HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
          ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ) /
      (↑(b - a) : ℂ) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      HMul.hMul (β := ℂ) (f b - f a)
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)

Tactic:
rw [div_eq_iff (ofReal_ne_zero.mpr hT.out.ne')]

Premises used: Iff.mpr, Complex.ofReal_ne_zero, LT.lt.ne', div_eq_iff, 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
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
s2 :
  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (b - a)))
    (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a))
⊢ (f b - f a) *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ 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) : ℂ)

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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
s2 :
  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (b - a)))
    (↑b : ℝ ⧸ AddSubgroup.zmultiples (b - a)) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a))
⊢ 1 / (↑(b - a) : ℂ) *
      ((↑(b - a) : ℂ) * (1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ))) *
        ∫ (x : ℝ) in a..b,
          HMul.hMul (β := ℂ) (f' x)
            ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((↑(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:
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), HasDerivAt f (f' 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)

Tactic:
fourierCoeffOn_of_hasDeriv_right hab hn hf (fun x hx ↦ hff' x hx |>.hasDerivWithinAt) hf'

Premises used: HasDerivAt.hasDerivWithinAt, fourierCoeffOn_of_hasDeriv_right
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ x ∈ [[a, b]], HasDerivAt f (f' 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)

Tactic:
fourierCoeffOn_of_hasDerivAt_Ioo hab hn
    (fun x hx ↦ hf x hx |>.continuousAt.continuousWithinAt)
    (fun x hx ↦ hf x <| mem_Icc_of_Ioo hx)
    hf'

Premises used: ContinuousAt.continuousWithinAt, Set.mem_Icc_of_Ioo, HasDerivAt.continuousAt, fourierCoeffOn_of_hasDerivAt_Ioo
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
⊢ Measure.IsAddHaarMeasure (G := UnitAddCircle) volume

Tactic:
inferInstanceAs (Measure.IsAddHaarMeasure AddCircle.haarAddCircle)

Premises used: _private.0.instIsAddHaarMeasureUnitAddCircleVolume._proof_1
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
⊢ IsProbabilityMeasure (α := UnitAddCircle) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
inferInstanceAs (IsProbabilityMeasure AddCircle.haarAddCircle)

Premises used: _private.0.instIsProbabilityMeasureUnitAddCircleVolume._proof_1
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
⊢ Continuous (Y := ℂ) fun (x : UnitAddTorus d) ↦ ∏ i : d, (fourier (n i) : (a : AddCircle 1) → ℂ) (x i)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
x : UnitAddTorus d
⊢ Eq (α := ℂ) ((mFourier (-n) : (a : UnitAddTorus d) → ℂ) x : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((mFourier n : (a : UnitAddTorus d) → ℂ) x : ℂ) : ℂ)

Tactic:
simp only [mFourier, Pi.neg_apply, fourier_neg, ContinuousMap.coe_mk, map_prod]

Premises used: map_prod, UnitAddTorus.mFourier, ContinuousMap.coe_mk, fourier_neg, Pi.neg_apply
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
x : UnitAddTorus d
m : d → ℤ
⊢ (mFourier (m + n) : (a : UnitAddTorus d) → ℂ) x =
    HMul.hMul (α := ℂ) (β := ℂ) ((mFourier m : (a : UnitAddTorus d) → ℂ) x : ℂ)
      ((mFourier n : (a : UnitAddTorus d) → ℂ) x : ℂ)

Tactic:
simp only [mFourier, Pi.add_apply, fourier_add, ContinuousMap.coe_mk, ← Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, Pi.add_apply, UnitAddTorus.mFourier, ContinuousMap.coe_mk, fourier_add
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
h :
  ∀ (x : UnitAddTorus d),
    Eq (α := ℂ) ((mFourier 0 : (a : UnitAddTorus d) → ℂ) x : ℂ) ((1 : (a : UnitAddTorus d) → ℂ) x : ℂ)
⊢ Eq.{u_1 + 1} (α := C(UnitAddTorus d, ℂ)) (mFourier 0) 1

Tactic:
ext x
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
x : UnitAddTorus d
⊢ Eq (α := ℂ) ((mFourier 0 : (a : UnitAddTorus d) → ℂ) x : ℂ) ((1 : (a : UnitAddTorus d) → ℂ) x : ℂ)

Tactic:
simp only [mFourier, Pi.zero_apply, fourier_zero, Finset.prod_const_one, ContinuousMap.coe_mk,
    ContinuousMap.one_apply]

Premises used: fourier_zero, ContinuousMap.one_apply, Pi.zero_apply, Finset.prod_const_one, UnitAddTorus.mFourier, ContinuousMap.coe_mk
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
a : ‖mFourier n‖ ≤ 1
a₁ : 1 ≤ ‖mFourier n‖
⊢ ‖mFourier n‖ = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
⊢ ‖mFourier n‖ ≤ 1

Tactic:
(ContinuousMap.norm_le _ zero_le_one).mpr fun i ↦ ?_

Premises used: Iff.mpr, ContinuousMap.norm_le, zero_le_one
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
a : ∀ (i : UnitAddTorus d), norm (E := ℂ) ((mFourier n : (a : UnitAddTorus d) → ℂ) i : ℂ) ≤ 1
⊢ ‖mFourier n‖ ≤ 1

Tactic:
refine (ContinuousMap.norm_le _ zero_le_one).mpr fun i ↦ ?_

Premises used: Iff.mpr, ContinuousMap.norm_le, zero_le_one
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
i : UnitAddTorus d
⊢ norm (E := ℂ) ((mFourier n : (a : UnitAddTorus d) → ℂ) i : ℂ) ≤ 1

Tactic:
simp only [mFourier, fourier_apply, ContinuousMap.coe_mk, norm_prod, Circle.norm_coe,
      Finset.prod_const_one, le_rfl]

Premises used: le_rfl, Circle.norm_coe, fourier_apply, Finset.prod_const_one, norm_prod, UnitAddTorus.mFourier, ContinuousMap.coe_mk
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
⊢ 1 ≤ ‖mFourier n‖

Tactic:
(le_of_eq ?_).trans ((mFourier n).norm_coe_le_norm fun _ ↦ 0)

Premises used: ContinuousMap.norm_coe_le_norm, UnitAddTorus.mFourier, LE.le.trans, le_of_eq, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
a : 1 = norm (E := ℂ) ((mFourier n : (a : UnitAddTorus d) → ℂ) fun (x : d) ↦ 0 : ℂ)
⊢ 1 ≤ ‖mFourier n‖

Tactic:
refine (le_of_eq ?_).trans ((mFourier n).norm_coe_le_norm fun _ ↦ 0)

Premises used: ContinuousMap.norm_coe_le_norm, UnitAddTorus.mFourier, LE.le.trans, le_of_eq, OfNat.ofNat