awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j : ZMod N
h :
  ∑ x : ZMod N, ∑ x_1 : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-((j + x_1) * x)) : ℂ) (Φ x_1) =
    HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
⊢ auxDFT (auxDFT Φ) j = HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))

Tactic:
simp only [auxDFT, mul_comm _ j, smul_sum, ← smul_assoc, smul_eq_mul, ← map_add_eq_mul, ←
    neg_add, ← add_mul]

Premises used: add_mul, smul_assoc, AddChar.map_add_eq_mul, neg_add, Finset.smul_sum, mul_comm, _private.0.ZMod.auxDFT, smul_eq_mul
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j : ZMod N
h :
  ∑ y : ZMod N, ∑ x : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-((j + y) * x)) : ℂ) (Φ y) =
    HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
⊢ ∑ x : ZMod N, ∑ x_1 : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-((j + x_1) * x)) : ℂ) (Φ x_1) =
    HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))

Tactic:
rw [sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j : ZMod N
h :
  ∑ x : ZMod N, HSMul.hSMul (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (-(j + x) * i)) (Φ x) =
    HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
⊢ ∑ y : ZMod N, ∑ x : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-((j + y) * x)) : ℂ) (Φ y) =
    HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))

Tactic:
simp only [← sum_smul, ← neg_mul]

Premises used: Finset.sum_smul, neg_mul
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
pos : ∀ (h : t = 0), Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) (↑N : ℂ)
neg : ∀ (h : ¬t = 0), Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) 0
⊢ Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) (if t = 0 then (↑N : ℂ) else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
h : t = 0
⊢ Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) (↑N : ℂ)

Tactic:
simp only [h, zero_mul, map_zero_eq_one, sum_const, card_univ, card,
        nsmul_eq_mul, mul_one]

Premises used: Finset.card_univ, MulZeroClass.zero_mul, AddChar.map_zero_eq_one, nsmul_eq_mul, mul_one, ZMod.card, Finset.sum_const
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
h : ¬t = 0
⊢ Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) 0

Tactic:
sum_eq_zero_of_ne_one (isPrimitive_stdAddChar N h)

Premises used: ZMod.isPrimitive_stdAddChar, AddChar.sum_eq_zero_of_ne_one
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
h : ¬t = 0
⊢ Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) 0

Tactic:
exact sum_eq_zero_of_ne_one (isPrimitive_stdAddChar N h)

Premises used: ZMod.isPrimitive_stdAddChar, AddChar.sum_eq_zero_of_ne_one
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ∀ (t : ZMod N), Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) (if t = 0 then (↑N : ℂ) else 0)

Tactic:
have h1 (t : ZMod N) : ∑ i, stdAddChar (t * i) = if t = 0 then ↑N else 0 := by
    split_ifs with h
    · simp only [h, zero_mul, map_zero_eq_one, sum_const, card_univ, card,
        nsmul_eq_mul, mul_one]
    · exact sum_eq_zero_of_ne_one (isPrimitive_stdAddChar N h)
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j_1 : ZMod N
h1 : ∀ (t : ZMod N), Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) (if t = 0 then (↑N : ℂ) else 0)
x j : ZMod N
rw : -j + -x = 0 ↔ x = -j
rw₁ : -x + -j = 0 ↔ x = -j
rw₂ : - -x = -j ↔ x = -j
rw₃ rw₄ : x = -j ↔ x = -j
⊢ -(j + x) = 0 ↔ x = -j

Tactic:
rw [neg_add, add_comm, add_eq_zero_iff_neg_eq, neg_neg]

Premises used: neg_add, neg_neg, add_comm, add_eq_zero_iff_neg_eq
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j : ZMod N
h1 : ∀ (t : ZMod N), Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) (if t = 0 then (↑N : ℂ) else 0)
⊢ ∀ (x j : ZMod N), -(j + x) = 0 ↔ x = -j

Tactic:
have h2 (x j : ZMod N) : -(j + x) = 0 ↔ x = -j := by
    rw [neg_add, add_comm, add_eq_zero_iff_neg_eq, neg_neg]
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j : ZMod N
h1 : ∀ (t : ZMod N), Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) (if t = 0 then (↑N : ℂ) else 0)
h2 : ∀ (x j : ZMod N), -(j + x) = 0 ↔ x = -j
⊢ ∑ x : ZMod N, HSMul.hSMul (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (-(j + x) * i)) (Φ x) =
    HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))

Tactic:
simp only [h1, h2, ite_smul, zero_smul, sum_ite_eq', mem_univ, ite_true]

Premises used: Finset.mem_univ, Finset.sum_ite_eq', ite_true, zero_smul, ite_smul
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
c : ℂ
Φ : ZMod N → E
h : ∀ (x : ZMod N), auxDFT (c • Φ) x = (c • auxDFT Φ) x
⊢ auxDFT (c • Φ) = c • auxDFT Φ

Tactic:
ext
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
c : ℂ
Φ : ZMod N → E
x : ZMod N
⊢ auxDFT (c • Φ) x = (c • auxDFT Φ) x

Tactic:
simp only [Pi.smul_def, auxDFT, smul_sum, smul_comm c]

Premises used: Finset.smul_sum, _private.0.ZMod.auxDFT, SMulCommClass.smul_comm, Pi.smul_def
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ₁ Φ₂ : ZMod N → E
h : ∀ (x : ZMod N), auxDFT (Φ₁ + Φ₂) x = (auxDFT Φ₁ + auxDFT Φ₂) x
⊢ auxDFT (Φ₁ + Φ₂) = auxDFT Φ₁ + auxDFT Φ₂

Tactic:
ext
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ₁ Φ₂ : ZMod N → E
x : ZMod N
⊢ auxDFT (Φ₁ + Φ₂) x = (auxDFT Φ₁ + auxDFT Φ₂) x

Tactic:
simp only [auxDFT, Pi.add_def, smul_add, sum_add_distrib]

Premises used: Finset.sum_add_distrib, Pi.add_def, _private.0.ZMod.auxDFT, smul_add
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
c : ℂ
Φ : ZMod N → E
h : ∀ (x : ZMod N), auxDFT (c • Φ) x = HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ) (auxDFT Φ) x
⊢ auxDFT (c • Φ) = HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ) (auxDFT Φ)

Tactic:
ext
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
c : ℂ
Φ : ZMod N → E
x : ZMod N
⊢ auxDFT (c • Φ) x = HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ) (auxDFT Φ) x

Tactic:
simp only [auxDFT, Pi.smul_apply, RingHom.id_apply, smul_sum, smul_comm c]

Premises used: RingHom.id_apply, Finset.smul_sum, _private.0.ZMod.auxDFT, SMulCommClass.smul_comm, Pi.smul_apply
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
⊢ (fun (Φ : ZMod N → E) (k : ZMod N) ↦ HSMul.hSMul (α := ℂ) (↑N : ℂ)⁻¹ (auxDFT Φ (-k))) (auxDFT Φ) = Φ

Tactic:
simp only [auxDFT_auxDFT, neg_neg, ← mul_smul, inv_mul_cancel₀ (NeZero.ne _), one_smul]

Premises used: neg_neg, _private.0.ZMod.auxDFT_auxDFT, one_smul, inv_mul_cancel₀, SemigroupAction.mul_smul, NeZero.ne
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
h :
  ∀ (j : ZMod N),
    auxDFT ((fun (Φ : ZMod N → E) (k : ZMod N) ↦ HSMul.hSMul (α := ℂ) (↑N : ℂ)⁻¹ (auxDFT Φ (-k))) Φ) j = Φ j
⊢ auxDFT ((fun (Φ : ZMod N → E) (k : ZMod N) ↦ HSMul.hSMul (α := ℂ) (↑N : ℂ)⁻¹ (auxDFT Φ (-k))) Φ) = Φ

Tactic:
ext1 j
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ auxDFT ((fun (Φ : ZMod N → E) (k : ZMod N) ↦ HSMul.hSMul (α := ℂ) (↑N : ℂ)⁻¹ (auxDFT Φ (-k))) Φ) j = Φ j

Tactic:
simp only [← Pi.smul_def, auxDFT_smul, auxDFT_neg, auxDFT_auxDFT, neg_neg, ← mul_smul,
      inv_mul_cancel₀ (NeZero.ne _), one_smul]

Premises used: _private.0.ZMod.auxDFT_smul, neg_neg, _private.0.ZMod.auxDFT_auxDFT, one_smul, _private.0.ZMod.auxDFT_neg, Pi.smul_def, inv_mul_cancel₀, SemigroupAction.mul_smul, NeZero.ne
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
k : ZMod N
⊢ Eq (α := E) ((𝓕 : (a : ZMod N → E) → ZMod N → E) Φ k : E)
    (∑ j : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ j) : E)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, _private.0.ZMod.auxDFT, Finset.sum, rfl
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
⊢ Eq (α := ZMod N → E) ((𝓕 : (a : ZMod N → E) → ZMod N → E) Φ : ZMod N → E) fun (k : ZMod N) ↦
    (∑ j : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ j) : E)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, _private.0.ZMod.auxDFT, Finset.sum, rfl
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Ψ : ZMod N → E
k : ZMod N
⊢ (LinearEquiv.symm 𝓕 : (a : ZMod N → E) → ZMod N → E) Ψ k =
    HSMul.hSMul (α := ℂ) (β := E) (↑N : ℂ)⁻¹
      (∑ j : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (j * k) : ℂ) (Ψ j))

Tactic:
simp only [dft, LinearEquiv.coe_symm_mk, auxDFT, mul_neg, neg_neg]

Premises used: ZMod.dft, neg_neg, LinearEquiv.coe_symm_mk, _private.0.ZMod.auxDFT, mul_neg
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Ψ : ZMod N → E
⊢ Eq (α := ZMod N → E) ((LinearEquiv.symm 𝓕 : (a : ZMod N → E) → ZMod N → E) Ψ : ZMod N → E) fun (k : ZMod N) ↦
    HSMul.hSMul (α := ℂ) (β := E) (↑N : ℂ)⁻¹
      (∑ j : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (j * k) : ℂ) (Ψ j))

Tactic:
funext <| invDFT_apply Ψ

Premises used: ZMod.invDFT_apply, funext
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Ψ : ZMod N → E
k : ZMod N
⊢ (LinearEquiv.symm 𝓕 : (a : ZMod N → E) → ZMod N → E) Ψ k =
    HSMul.hSMul (α := ℂ) (β := E) (↑N : ℂ)⁻¹ ((𝓕 : (a : ZMod N → E) → ZMod N → E) Ψ (-k) : E)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, _private.0.ZMod.auxDFT, Finset.sum, rfl
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Ψ : ZMod N → E
⊢ Eq (α := ZMod N → E) ((LinearEquiv.symm 𝓕 : (a : ZMod N → E) → ZMod N → E) Ψ : ZMod N → E) fun (k : ZMod N) ↦
    HSMul.hSMul (α := ℂ) (β := E) (↑N : ℂ)⁻¹ ((𝓕 : (a : ZMod N → E) → ZMod N → E) Ψ (-k) : E)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, _private.0.ZMod.auxDFT, Finset.sum, rfl
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
⊢ Eq (α := E) ((𝓕 : (a : ZMod N → E) → ZMod N → E) Φ 0 : E) (∑ j : ZMod N, Φ j : E)

Tactic:
simp only [dft_apply, mul_zero, neg_zero, map_zero_eq_one, one_smul]

Premises used: AddChar.map_zero_eq_one, ZMod.dft_apply, one_smul, MulZeroClass.mul_zero, neg_zero
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : CompleteSpace E
Φ : ZMod N → E
k : ZMod N
⊢ (𝓕 : (a : ZMod N → E) → ZMod N → E) Φ k = Fourier.fourierIntegral toCircle Measure.count Φ k

Tactic:
simp only [dft_apply, stdAddChar_apply, Fourier.fourierIntegral_def, Circle.smul_def,
    integral_countable <| .of_finite .., count_real_singleton, one_smul, tsum_fintype]

Premises used: Circle.smul_def, ZMod.dft_apply, one_smul, tsum_fintype, MeasureTheory.integral_countable, Fourier.fourierIntegral_def, MeasureTheory.count_real_singleton, ZMod.stdAddChar_apply
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
R : Type u_2
inst_3 : DistribSMul R E
inst_4 : SMulCommClass R ℂ E
r : R
Φ : ZMod N → E
⊢ (𝓕 : (a : ZMod N → E) → ZMod N → E) (r • Φ) =
    HSMul.hSMul (β := ZMod N → E) r ((𝓕 : (a : ZMod N → E) → ZMod N → E) Φ : ZMod N → E)

Tactic:
simp only [Pi.smul_def, dft_def, smul_sum, smul_comm]

Premises used: Finset.smul_sum, SMulCommClass.smul_comm, Pi.smul_def, ZMod.dft_def
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
R : Type u_2
inst_3 : Ring R
inst_4 : Module ℂ R
inst_5 : Module R E
inst_6 : IsScalarTower ℂ R E
Φ : ZMod N → R
e : E
⊢ Eq.{u_1 + 1} (α := ZMod N → E) ((𝓕 : (a : ZMod N → E) → ZMod N → E) fun (j : ZMod N) ↦ Φ j • e : ZMod N → E)
    fun (k : ZMod N) ↦ HSMul.hSMul (α := R) ((𝓕 : (a : ZMod N → R) → ZMod N → R) Φ k : R) e

Tactic:
simp only [dft_def, sum_smul, smul_assoc]

Premises used: Finset.sum_smul, smul_assoc, ZMod.dft_def
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
R : Type u_2
inst_1 : Ring R
inst_2 : Algebra ℂ R
r : R
Φ : ZMod N → R
⊢ Eq.{u_2 + 1} (α := ZMod N → R) ((𝓕 : (a : ZMod N → R) → ZMod N → R) fun (j : ZMod N) ↦ r * Φ j : ZMod N → R)
    fun (k : ZMod N) ↦ HMul.hMul (β := R) r ((𝓕 : (a : ZMod N → R) → ZMod N → R) Φ k : R)

Tactic:
dft_const_smul r Φ

Premises used: ZMod.dft_const_smul
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
R : Type u_2
inst_1 : Ring R
inst_2 : Algebra ℂ R
Φ : ZMod N → R
r : R
⊢ Eq.{u_2 + 1} (α := ZMod N → R) ((𝓕 : (a : ZMod N → R) → ZMod N → R) fun (j : ZMod N) ↦ Φ j * r : ZMod N → R)
    fun (k : ZMod N) ↦ HMul.hMul (α := R) ((𝓕 : (a : ZMod N → R) → ZMod N → R) Φ k : R) r

Tactic:
dft_smul_const Φ r

Premises used: ZMod.dft_smul_const
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
⊢ Eq.{u_1 + 1} (α := ZMod N → E) ((𝓕 : (a : ZMod N → E) → ZMod N → E) fun (j : ZMod N) ↦ Φ (-j) : ZMod N → E)
    fun (k : ZMod N) ↦ ((𝓕 : (a : ZMod N → E) → ZMod N → E) Φ (-k) : E)

Tactic:
auxDFT_neg ..

Premises used: Multiset.sum, Multiset.foldr, _private.0.ZMod.auxDFT, _private.0.ZMod.auxDFT_neg, Finset.sum
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
⊢ Eq (α := ZMod N → E)
    ((𝓕 : (a : ZMod N → E) → ZMod N → E) ((𝓕 : (a : ZMod N → E) → ZMod N → E) Φ : ZMod N → E) : ZMod N → E)
    fun (j : ZMod N) ↦ HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))

Tactic:
auxDFT_auxDFT ..

Premises used: Multiset.sum, Multiset.foldr, _private.0.ZMod.auxDFT_auxDFT, _private.0.ZMod.auxDFT, Finset.sum
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
u : (ZMod N)ˣ
k : ZMod N
⊢ Eq (α := E) ((𝓕 : (a : ZMod N → E) → ZMod N → E) (fun (j : ZMod N) ↦ Φ ((↑u : ZMod N) * j)) k : E)
    ((𝓕 : (a : ZMod N → E) → ZMod N → E) Φ ((↑u⁻¹ : ZMod N) * k) : E)

Tactic:
Fintype.sum_equiv u.mulLeft _ _ fun x ↦ ?_

Premises used: Multiset.sum, Multiset.foldr, _private.0.ZMod.auxDFT, Fintype.sum_equiv, Units.mulLeft, Finset.sum
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
u : (ZMod N)ˣ
k : ZMod N
refine :
  ∀ (x : ZMod N),
    HSMul.hSMul (α := ℂ) (β := E) ((stdAddChar : (a : ZMod N) → ℂ) (-(x * k)) : ℂ)
        ((fun (j : ZMod N) ↦ Φ ((↑u : ZMod N) * j)) x) =
      HSMul.hSMul (α := ℂ)
        ((stdAddChar : (a : ZMod N) → ℂ)
            (-HMul.hMul (α := ZMod N) ((u.mulLeft : (a : ZMod N) → ZMod N) x : ZMod N) ((↑u⁻¹ : ZMod N) * k)) :
          ℂ)
        (Φ ((u.mulLeft : (a : ZMod N) → ZMod N) x))
⊢ Eq (α := E) ((𝓕 : (a : ZMod N → E) → ZMod N → E) (fun (j : ZMod N) ↦ Φ ((↑u : ZMod N) * j)) k : E)
    ((𝓕 : (a : ZMod N → E) → ZMod N → E) Φ ((↑u⁻¹ : ZMod N) * k) : E)

Tactic:
refine Fintype.sum_equiv u.mulLeft _ _ fun x ↦ ?_

Premises used: Fintype.sum_equiv, Units.mulLeft
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
u : (ZMod N)ˣ
k x : ZMod N
⊢ HSMul.hSMul (α := ℂ) (β := E) ((stdAddChar : (a : ZMod N) → ℂ) (-(x * k)) : ℂ)
      ((fun (j : ZMod N) ↦ Φ ((↑u : ZMod N) * j)) x) =
    HSMul.hSMul (α := ℂ)
      ((stdAddChar : (a : ZMod N) → ℂ)
          (-HMul.hMul (α := ZMod N) ((u.mulLeft : (a : ZMod N) → ZMod N) x : ZMod N) ((↑u⁻¹ : ZMod N) * k)) :
        ℂ)
      (Φ ((u.mulLeft : (a : ZMod N) → ZMod N) x))

Tactic:
simp only [mul_comm u.val, u.mulLeft_apply, ← mul_assoc, u.mul_inv_cancel_right]

Premises used: Units.val, mul_assoc, Units.mul_inv_cancel_right, Units.mulLeft_apply, mul_comm
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ f : ZMod N → ℂ
hf : Function.Even f
⊢ Function.Even (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) f)

Tactic:
simp only [Function.Even, ← congr_fun (dft_comp_neg f), funext hf, implies_true]

Premises used: Function.Even, ZMod.dft_comp_neg, funext, implies_true, congr_fun
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
⊢ ∀ {f : ZMod N → ℂ} (hf : Function.Even f),
    Function.Even (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) f)

Tactic:
have h {f : ZMod N → ℂ} (hf : f.Even) : (𝓕 f).Even := by
    simp only [Function.Even, ← congr_fun (dft_comp_neg f), funext hf, implies_true]
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
h :
  ∀ {f : ZMod N → ℂ} (hf : Function.Even f),
    Function.Even (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) f)
⊢ Function.Even (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) ↔ Function.Even Φ

Tactic:
⟨fun hΦ x ↦ ?_, h⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
h :
  ∀ {f : ZMod N → ℂ} (hf : Function.Even f),
    Function.Even (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) f)
refine :
  ∀ (hΦ : Function.Even (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ)) (x : ZMod N), Φ (-x) = Φ x
⊢ Function.Even (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) ↔ Function.Even Φ

Tactic:
refine ⟨fun hΦ x ↦ ?_, h⟩
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
h :
  ∀ {f : ZMod N → ℂ} (hf : Function.Even f),
    Function.Even (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) f)
hΦ : Function.Even (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ)
x : ZMod N
⊢ Φ (-x) = Φ x

Tactic:
simpa only [neg_neg, smul_right_inj (NeZero.ne (N : ℂ)), dft_dft] using h hΦ (-x)

Premises used: neg_neg, Nat.cast, ZMod.dft_dft, smul_right_inj, Neg.neg, NeZero.ne
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ f : ZMod N → ℂ
hf : Function.Odd f
⊢ Function.Odd (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) f)

Tactic:
simp only [Function.Odd, ← congr_fun (dft_comp_neg f), funext hf, ← Pi.neg_apply, map_neg,
      implies_true]

Premises used: Function.Odd, map_neg, ZMod.dft_comp_neg, funext, implies_true, congr_fun, Pi.neg_apply
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
⊢ ∀ {f : ZMod N → ℂ} (hf : Function.Odd f), Function.Odd (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) f)

Tactic:
have h {f : ZMod N → ℂ} (hf : f.Odd) : (𝓕 f).Odd := by
    simp only [Function.Odd, ← congr_fun (dft_comp_neg f), funext hf, ← Pi.neg_apply, map_neg,
      implies_true]
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
h :
  ∀ {f : ZMod N → ℂ} (hf : Function.Odd f), Function.Odd (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) f)
⊢ Function.Odd (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) ↔ Function.Odd Φ

Tactic:
⟨fun hΦ x ↦ ?_, h⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
h :
  ∀ {f : ZMod N → ℂ} (hf : Function.Odd f), Function.Odd (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) f)
refine :
  ∀ (hΦ : Function.Odd (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ)) (x : ZMod N), Φ (-x) = -Φ x
⊢ Function.Odd (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) ↔ Function.Odd Φ

Tactic:
refine ⟨fun hΦ x ↦ ?_, h⟩
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
h :
  ∀ {f : ZMod N → ℂ} (hf : Function.Odd f), Function.Odd (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) f)
hΦ : Function.Odd (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ)
x : ZMod N
⊢ Φ (-x) = -Φ x

Tactic:
simpa only [neg_neg, dft_dft, ← smul_neg, smul_right_inj (NeZero.ne (N : ℂ))] using h hΦ (-x)

Premises used: neg_neg, smul_neg, Nat.cast, ZMod.dft_dft, smul_right_inj, Neg.neg, NeZero.ne
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
k : ZMod N
simp :
  ∑ x : ZMod N,
      HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(x * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) x : ℂ) =
    gaussSum χ (mulShift stdAddChar (-k))
⊢ (𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ) k = gaussSum χ (mulShift stdAddChar (-k))

Tactic:
simp only [dft_apply, smul_eq_mul]

Premises used: ZMod.dft_apply, smul_eq_mul
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
k : ZMod N
e_f :
  ∀ (j : ZMod N),
    HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
      HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((mulShift stdAddChar (-k) : (a : ZMod N) → ℂ) j : ℂ)
⊢ ∑ x : ZMod N,
      HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(x * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) x : ℂ) =
    gaussSum χ (mulShift stdAddChar (-k))

Tactic:
congr 1 with j