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)
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) : ℂ) *
      (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 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)) : ℂ)))
Tactic: rw [s2, intervalIntegral.integral_const_mul, ← sub_mul, mul_sub, mul_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
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) : ℂ) *
        ((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)) : ℂ)))
have 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)) : ℂ)
Tactic: congr 1
-- 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)
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)) : ℂ)
⊢ 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)) : ℂ)))
have 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)) : ℂ)))
Tactic: congr 1
-- 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)
s2 :
  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (b - a)))
    (↑b : ℝ ⧸ AddSubgroup.zmultiples (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)) : ℂ))
have 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) : ℂ)
Tactic: rw [mul_comm, mul_div, mul_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)
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) : ℂ) *
      ((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)) : ℂ)
have 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)) : ℂ)
Tactic: conv_lhs => rw [mul_comm, mul_div, mul_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)
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)) : ℂ) /
      (↑(b - a) : ℂ) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      HMul.hMul (β := ℂ) (f b - f a)
        ((fourier (-n) : (a : AddCircle (b - a)) → ℂ) (↑a : ℝ ⧸ AddSubgroup.zmultiples (b - a)) : ℂ)
have 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) : ℂ)
Tactic: rw [div_eq_iff (ofReal_ne_zero.mpr hT.out.ne')]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
⊢ Eq.{u_1 + 1} (α := C(UnitAddTorus d, ℂ)) (mFourier 0) 1
have h : ∀ (x : UnitAddTorus d),
  Eq (α := ℂ) ((mFourier 0 : (a : UnitAddTorus d) → ℂ) x : ℂ) ((1 : (a : UnitAddTorus d) → ℂ) x : ℂ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
⊢ ‖mFourier n‖ = 1
have a : ‖mFourier n‖ ≤ 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
a : ‖mFourier n‖ ≤ 1
⊢ ‖mFourier n‖ = 1
have a₁ : 1 ≤ ‖mFourier n‖
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
⊢ ‖mFourier n‖ ≤ 1
have a : ∀ (i : UnitAddTorus d), norm (E := ℂ) ((mFourier n : (a : UnitAddTorus d) → ℂ) i : ℂ) ≤ 1
Tactic: refine (ContinuousMap.norm_le _ zero_le_one).mpr fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
n : d → ℤ
⊢ 1 ≤ ‖mFourier n‖
have a : 1 = norm (E := ℂ) ((mFourier n : (a : UnitAddTorus d) → ℂ) fun (x : d) ↦ 0 : ℂ)
Tactic: refine (le_of_eq ?_).trans ((mFourier n).norm_coe_le_norm fun _ ↦ 0)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
⊢ Eq (α := ℂ) ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) z : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
have simp_rw : Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
  ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
Tactic: simp_rw [mFourier, ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (hypothesis)
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
⊢ Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
have this : HMul.hMul (α := ℂ) (∏ i_1 ∈ {i}, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
    (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)) =
  ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
Tactic: have := Finset.prod_mul_prod_compl {i} (fun j ↦ fourier ((Pi.single i (1 : ℤ) : d → ℤ) j) (z j))
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this :
  HMul.hMul (α := ℂ) (∏ i_1 ∈ {i}, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
⊢ Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
have rw : ∀
  (this :
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
        (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
      ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
  (this :
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
        (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
      ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)),
  Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
Tactic: rw [Finset.prod_singleton, Finset.prod_congr rfl (fun j hj ↦ ?_)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this :
  HMul.hMul (α := ℂ) (∏ i_1 ∈ {i}, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
rw :
  ∀
    (this :
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
          (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
        ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
    (this :
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
          (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
        ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)),
    Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
      ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
⊢ Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
have rw₁ : (this :
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
        (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
      ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)) →
  d → ℂ
Tactic: rw [Finset.prod_singleton, Finset.prod_congr rfl (fun j hj ↦ ?_)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this :
  HMul.hMul (α := ℂ) (∏ i_1 ∈ {i}, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
rw :
  ∀
    (this :
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
          (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
        ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
    (this :
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
          (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
        ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)),
    Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
      ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
rw₁ :
  (this :
      HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
          (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
        ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)) →
    d → ℂ
⊢ Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
have rw₂ : ∀
  (this :
    HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
        (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
      ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1))
  (j : d) (hj : Membership.mem (γ := Finset d) {i}ᶜ j),
  Eq (α := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 j) : (a : AddCircle 1) → ℂ) (z j) : ℂ) (1 : ℂ)
Tactic: rw [Finset.prod_singleton, Finset.prod_congr rfl (fun j hj ↦ ?_)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this_1 :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
this :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
⊢ Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
have rw : HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
    (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
  (fourier 1 : (a : AddCircle 1) → ℂ) (z i)
Tactic: rw [← this, Finset.prod_const_one, mul_one, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this_1 :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
this :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
rw :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
    (fourier 1 : (a : AddCircle 1) → ℂ) (z i)
⊢ Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
have rw₁ : HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
    (1 : ℂ) =
  (fourier 1 : (a : AddCircle 1) → ℂ) (z i)
Tactic: rw [← this, Finset.prod_const_one, mul_one, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this_1 :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
this :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
rw :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
    (fourier 1 : (a : AddCircle 1) → ℂ) (z i)
rw₁ :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (1 : ℂ) =
    (fourier 1 : (a : AddCircle 1) → ℂ) (z i)
⊢ Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
have rw₂ : Eq (α := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
  ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
Tactic: rw [← this, Finset.prod_const_one, mul_one, Pi.single_eq_same]