awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (β := ℂ) (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)))
have pattern₁ : HMul.hMul (β := ℂ) (f b - f a)
  ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: pattern (occs := 1 2 3) fourier _ _ * _ <;> (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)
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)) : ℂ)
| 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])
-- 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 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)) : ℂ)))
Tactic: conv => pattern (occs := 1 2 3) fourier _ _ * _ <;> (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 (β := ℂ) (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)) : ℂ)))
have 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)) : ℂ)))
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 _ _)]
-- 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
hT : Fact (0 < 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)) : ℂ)))
have this : ∀ (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
-- 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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
| ∫ (x : ℝ) in a..b,
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
have f₁ : fun (x : ℝ) ↦
  f' x *
    HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
      ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: congr
-- 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)
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)) : ℂ)
| ∫ (x : ℝ) in a..b,
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
have a₁ : a
Tactic: congr
-- 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)
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
| ∫ (x : ℝ) in a..b,
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
have b₁ : b
Tactic: congr
-- 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)
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
| ∫ (x : ℝ) in a..b,
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
have μ : volume
Tactic: congr
-- 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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
| fun (x : ℝ) ↦
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
have f₁ : ∀ (x : ℝ),
  f' x *
    HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
      ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: ext
-- 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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
x : ℝ
| f' x *
    HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
      ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
have f₁ : (↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
  HMul.hMul (β := ℂ) (f' x) ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: rw [this]
-- 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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
| ∫ (x : ℝ) in a..b,
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
have f₁ : ∀ (x : ℝ),
  (↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
    HMul.hMul (β := ℂ) (f' x)
      ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
Tactic: congr; ext; rw [this]
-- 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)
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)) : ℂ)
| ∫ (x : ℝ) in a..b,
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
have a₁ : a
Tactic: congr; ext; rw [this]
-- 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)
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
| ∫ (x : ℝ) in a..b,
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
have b₁ : b
Tactic: congr; ext; rw [this]
-- 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)
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
| ∫ (x : ℝ) in a..b,
    f' x *
      HMul.hMul (β := ℂ) ((↑(b - a) : ℂ) / (-2 * (↑π : ℂ) * I * (↑n : ℂ)))
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
have μ : volume
Tactic: congr; ext; rw [this]
-- 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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
⊢ 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)) : ℂ)))
have 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)) : ℂ)))
Tactic: conv in intervalIntegral _ _ _ _ => congr; ext; rw [this]
-- 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)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
⊢ 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)) : ℂ)))
have 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)) : ℂ)))
Tactic: rw [(by ring : ((b - a : ℝ) : ℂ) / (-2 * π * I * n) = ((b - a : ℝ) : ℂ) * (1 / (-2 * π * I * n)))]
-- 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
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * ((↑(b - a) : ℂ) / v * w) = (↑(b - a) : ℂ) / v * (u * w)
⊢ 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)) : ℂ)))
have s2 : 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