awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
inst_6 : CompleteSpace E
inst_7 : CompleteSpace E'
inst_8 : CompleteSpace F
μ ν : Measure ℝ
inst_9 : SFinite μ
inst_10 : SFinite ν
inst_11 : μ.IsAddRightInvariant
inst_12 : NoAtoms ν
f : ℝ → E
g : ℝ → E'
hf : IntegrableOn f (Ioi 0) ν
hg : IntegrableOn g (Ioi 0) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Eq.{uF + 1} (α := F)
    (∫ (x : ℝ) in Ioi 0,
        ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν ∂μ :
      F)
    (((L : (a : E) → E' →L[ℝ] F) (∫ (x : ℝ) in Ioi 0, f x ∂ν) : (a : E') → F) (∫ (x : ℝ) in Ioi 0, g x ∂μ) : F)
have rw : ∀ (hf : Integrable (indicator (Ioi 0) f) ν) (hg : Integrable (indicator (Ioi 0) g) μ) (L : E →L[ℝ] E' →L[ℝ] F),
  Eq.{uF + 1} (α := F)
    (∫ (x : ℝ) in Ioi 0,
        ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν ∂μ :
      F)
    (((L : (a : E) → E' →L[ℝ] F) (∫ (x : ℝ) in Ioi 0, f x ∂ν) : (a : E') → F) (∫ (x : ℝ) in Ioi 0, g x ∂μ) : F)
Tactic: rw [← integrable_indicator_iff measurableSet_Ioi] at hf hg
Cleared hypotheses: hf, hg, L
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
inst_6 : CompleteSpace E
inst_7 : CompleteSpace E'
inst_8 : CompleteSpace F
μ ν : Measure ℝ
inst_9 : SFinite μ
inst_10 : SFinite ν
inst_11 : μ.IsAddRightInvariant
inst_12 : NoAtoms ν
f : ℝ → E
g : ℝ → E'
hf : Integrable (indicator (Ioi 0) f) ν
hg : Integrable (indicator (Ioi 0) g) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Eq.{uF + 1} (α := F)
    (∫ (x : ℝ) in Ioi 0,
        ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν ∂μ :
      F)
    (((L : (a : E) → E' →L[ℝ] F) (∫ (x : ℝ) in Ioi 0, f x ∂ν) : (a : E') → F) (∫ (x : ℝ) in Ioi 0, g x ∂μ) : F)
have simp_rw : Eq.{uF + 1} (α := F)
  (∫ (x : ℝ),
      indicator (Ioi 0)
        (fun (x : ℝ) ↦
          ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν)
        x ∂μ :
    F)
  (((L : (a : E) → E' →L[ℝ] F) (∫ (x : ℝ), indicator (Ioi 0) f x ∂ν) : (a : E') → F)
      (∫ (x : ℝ), indicator (Ioi 0) g x ∂μ) :
    F)
Tactic: simp_rw [← integral_indicator measurableSet_Ioi]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
inst_6 : CompleteSpace E
inst_7 : CompleteSpace E'
inst_8 : CompleteSpace F
μ ν : Measure ℝ
inst_9 : SFinite μ
inst_10 : SFinite ν
inst_11 : μ.IsAddRightInvariant
inst_12 : NoAtoms ν
f : ℝ → E
g : ℝ → E'
hf : Integrable (indicator (Ioi 0) f) ν
hg : Integrable (indicator (Ioi 0) g) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Eq.{uF + 1} (α := F)
    (∫ (x : ℝ),
        indicator (Ioi 0)
          (fun (x : ℝ) ↦
            ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν)
          x ∂μ :
      F)
    (((L : (a : E) → E' →L[ℝ] F) (∫ (x : ℝ), indicator (Ioi 0) f x ∂ν) : (a : E') → F)
        (∫ (x : ℝ), indicator (Ioi 0) g x ∂μ) :
      F)
have h : ∀ (x : ℝ),
  (indicator (Ioi 0) fun (x : ℝ) ↦
      ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν) =
    indicator (Ioi 0) f ⋆[L, ν] indicator (Ioi 0) g
Tactic: convert! integral_convolution L hf hg using 4 with x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
⊢ Eq.{u_1 + 1} (α := (k : ZMod N) → E) (auxDFT fun (j : ZMod N) ↦ Φ (-j)) fun (k : ZMod N) ↦ auxDFT Φ (-k)
have h : ∀ (k : ZMod N), auxDFT (fun (j : ZMod N) ↦ Φ (-j)) k = auxDFT Φ (-k)
Tactic: ext1 k
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
k j : ZMod N
⊢ HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ (-j)) =
    HSMul.hSMul (α := ℂ)
      ((stdAddChar : (a : ZMod N) → ℂ)
          (-HMul.hMul (α := ZMod N) ((Equiv.neg (ZMod N) : (a : ZMod N) → ZMod N) j : ZMod N) (-k)) :
        ℂ)
      (Φ ((Equiv.neg (ZMod N) : (a : ZMod N) → ZMod N) j))
have rw : HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ (-j)) =
  HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(-j * -k)) : ℂ) (Φ (-j))
Tactic: rw [Equiv.neg_apply, neg_mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
k j : ZMod N
rw :
  HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ (-j)) =
    HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(-j * -k)) : ℂ) (Φ (-j))
⊢ HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ (-j)) =
    HSMul.hSMul (α := ℂ)
      ((stdAddChar : (a : ZMod N) → ℂ)
          (-HMul.hMul (α := ZMod N) ((Equiv.neg (ZMod N) : (a : ZMod N) → ZMod N) j : ZMod N) (-k)) :
        ℂ)
      (Φ ((Equiv.neg (ZMod N) : (a : ZMod N) → ZMod N) j))
have rw₁ : HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ (-j)) =
  HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ (-j))
Tactic: rw [Equiv.neg_apply, neg_mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
⊢ auxDFT (auxDFT Φ) = fun (j : ZMod N) ↦ HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
have h : ∀ (j : ZMod N), auxDFT (auxDFT Φ) j = HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
Tactic: ext1 j
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ auxDFT (auxDFT Φ) j = HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
have h : ∑ x : ZMod N, ∑ x_1 : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-((j + x_1) * x)) : ℂ) (Φ x_1) =
  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]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ∑ x : ZMod N, ∑ x_1 : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-((j + x_1) * x)) : ℂ) (Φ x_1) =
    HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
have h : ∑ y : ZMod N, ∑ x : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-((j + y) * x)) : ℂ) (Φ y) =
  HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
Tactic: rw [sum_comm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ∑ y : ZMod N, ∑ x : ZMod N, HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-((j + y) * x)) : ℂ) (Φ y) =
    HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
have h : ∑ x : ZMod N, HSMul.hSMul (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (-(j + x) * i)) (Φ x) =
  HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
Tactic: simp only [← sum_smul, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
⊢ Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) (if t = 0 then (↑N : ℂ) else 0)
have pos : ∀ (h : t = 0), Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) (↑N : ℂ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
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 : ℂ)
⊢ Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) (if t = 0 then (↑N : ℂ) else 0)
have neg : ∀ (h : ¬t = 0), Eq (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (t * i)) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (hypothesis)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ∑ x : ZMod N, HSMul.hSMul (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (-(j + x) * i)) (Φ x) =
    HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
have h1 : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
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
⊢ -(j + x) = 0 ↔ x = -j
have rw : -j + -x = 0 ↔ x = -j
Tactic: rw [neg_add, add_comm, add_eq_zero_iff_neg_eq, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
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
⊢ -(j + x) = 0 ↔ x = -j
have rw₁ : -x + -j = 0 ↔ x = -j
Tactic: rw [neg_add, add_comm, add_eq_zero_iff_neg_eq, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
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
⊢ -(j + x) = 0 ↔ x = -j
have rw₂ : - -x = -j ↔ x = -j
Tactic: rw [neg_add, add_comm, add_eq_zero_iff_neg_eq, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
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
⊢ -(j + x) = 0 ↔ x = -j
have rw₃ : x = -j ↔ x = -j
Tactic: rw [neg_add, add_comm, add_eq_zero_iff_neg_eq, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (hypothesis)
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 : ZMod N, HSMul.hSMul (α := ℂ) (∑ i : ZMod N, (stdAddChar : (a : ZMod N) → ℂ) (-(j + x) * i)) (Φ x) =
    HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
have h2 : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
c : ℂ
Φ : ZMod N → E
⊢ auxDFT (c • Φ) = c • auxDFT Φ
have h : ∀ (x : ZMod N), auxDFT (c • Φ) x = (c • auxDFT Φ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ₁ Φ₂ : ZMod N → E
⊢ auxDFT (Φ₁ + Φ₂) = auxDFT Φ₁ + auxDFT Φ₂
have h : ∀ (x : ZMod N), auxDFT (Φ₁ + Φ₂) x = (auxDFT Φ₁ + auxDFT Φ₂) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
c : ℂ
Φ : ZMod N → E
⊢ auxDFT (c • Φ) = HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ) (auxDFT Φ)
have h : ∀ (x : ZMod N), auxDFT (c • Φ) x = HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ) (auxDFT Φ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
⊢ auxDFT ((fun (Φ : ZMod N → E) (k : ZMod N) ↦ HSMul.hSMul (α := ℂ) (↑N : ℂ)⁻¹ (auxDFT Φ (-k))) Φ) = Φ
have h : ∀ (j : ZMod N), auxDFT ((fun (Φ : ZMod N → E) (k : ZMod N) ↦ HSMul.hSMul (α := ℂ) (↑N : ℂ)⁻¹ (auxDFT Φ (-k))) Φ) j = Φ j
Tactic: ext1 j
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
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)
have 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))
Tactic: refine Fintype.sum_equiv u.mulLeft _ _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (hypothesis)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
⊢ Function.Even (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) ↔ Function.Even Φ
have h : ∀ {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]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
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 Φ
have refine : ∀ (hΦ : Function.Even (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ)) (x : ZMod N), Φ (-x) = Φ x
Tactic: refine ⟨fun hΦ x ↦ ?_, h⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (hypothesis)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
⊢ Function.Odd (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) ↔ Function.Odd Φ
have h : ∀ {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]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
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 Φ
have refine : ∀ (hΦ : Function.Odd (α := ZMod N) (β := ℂ) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ)) (x : ZMod N), Φ (-x) = -Φ x
Tactic: refine ⟨fun hΦ x ↦ ?_, h⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
k : ZMod N
⊢ (𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ) k = gaussSum χ (mulShift stdAddChar (-k))
have simp : ∑ x : ZMod N,
    HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(x * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) x : ℂ) =
  gaussSum χ (mulShift stdAddChar (-k))
Tactic: simp only [dft_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
k : ZMod N
⊢ ∑ x : ZMod N,
      HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(x * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) x : ℂ) =
    gaussSum χ (mulShift stdAddChar (-k))
have 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 : ℂ)
Tactic: congr 1 with j
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
k 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 : ℂ)
have e_f : HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-k * j) : ℂ)
Tactic: rw [mulShift_apply, mul_comm j, neg_mul, stdAddChar_apply, mul_comm (χ _)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
k j : ZMod N
e_f :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-k * j) : ℂ)
⊢ 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 : ℂ)
have e_f₁ : HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-k * j) : ℂ)
Tactic: rw [mulShift_apply, mul_comm j, neg_mul, stdAddChar_apply, mul_comm (χ _)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
k j : ZMod N
e_f :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-k * j) : ℂ)
e_f₁ :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-k * j) : ℂ)
⊢ 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 : ℂ)
have e_f₂ : HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ)
Tactic: rw [mulShift_apply, mul_comm j, neg_mul, stdAddChar_apply, mul_comm (χ _)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
k j : ZMod N
e_f :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-k * j) : ℂ)
e_f₁ :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-k * j) : ℂ)
e_f₂ :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ)
⊢ 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 : ℂ)
have e_f₃ : HMul.hMul (α := ℂ) (β := ℂ) ((↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) : ℂ)
    ((χ : (a : ZMod N) → ℂ) j : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ)
    ((↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) : ℂ)
Tactic: rw [mulShift_apply, mul_comm j, neg_mul, stdAddChar_apply, mul_comm (χ _)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
k j : ZMod N
e_f :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-k * j) : ℂ)
e_f₁ :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-k * j) : ℂ)
e_f₂ :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ)
e_f₃ :
  HMul.hMul (α := ℂ) (β := ℂ) ((↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) : ℂ)
      ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ)
      ((↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) : ℂ)
⊢ 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 : ℂ)
have e_f₄ : HMul.hMul (α := ℂ) (β := ℂ) ((↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) : ℂ)
    ((χ : (a : ZMod N) → ℂ) j : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) : ℂ)
    ((χ : (a : ZMod N) → ℂ) j : ℂ)
Tactic: rw [mulShift_apply, mul_comm j, neg_mul, stdAddChar_apply, mul_comm (χ _)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
k : ZMod N
⊢ (𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ) k =
    HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-k) : ℂ) (gaussSum χ stdAddChar)
have rw : gaussSum χ (mulShift stdAddChar (-k)) = HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-k) : ℂ) (gaussSum χ stdAddChar)
Tactic: rw [fourierTransform_eq_gaussSum_mulShift, gaussSum_mulShift_of_isPrimitive _ hχ]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
k : ZMod N
rw :
  gaussSum χ (mulShift stdAddChar (-k)) = HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-k) : ℂ) (gaussSum χ stdAddChar)
⊢ (𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ) k =
    HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-k) : ℂ) (gaussSum χ stdAddChar)
have rw₁ : HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-k) : ℂ) (gaussSum χ stdAddChar) =
  HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-k) : ℂ) (gaussSum χ stdAddChar)
Tactic: rw [fourierTransform_eq_gaussSum_mulShift, gaussSum_mulShift_of_isPrimitive _ hχ]