-- Mathlib/Analysis/Fourier/ZMod.lean
/-- Fourier inversion formula, discrete case. -/
private lemma auxDFT_auxDFT (Φ : ZMod N → E) : auxDFT (auxDFT Φ) = fun j ↦ (N : ℂ) • Φ (-j)

Proof state:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ∑ y : ZMod N, ∑ x : ZMod N, stdAddChar (-((j + y) * x)) • Φ y = ↑N • Φ (-j)

Tactic:
simp only [← sum_smul, ← neg_mul]

Result:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ∑ x : ZMod N, (∑ i : ZMod N, stdAddChar (-(j + x) * i)) • Φ x = ↑N • Φ (-j)

Proof state:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
⊢ ZMod.auxDFT (ZMod.auxDFT Φ) = fun j => ↑N • Φ (-j)

Tactic:
ext1 j

Result:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ZMod.auxDFT (ZMod.auxDFT Φ) j = ↑N • Φ (-j)

Proof state:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ZMod.auxDFT (ZMod.auxDFT Φ) j = ↑N • Φ (-j)

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

Result:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ∑ x : ZMod N, ∑ x_1 : ZMod N, stdAddChar (-((j + x_1) * x)) • Φ x_1 = ↑N • Φ (-j)

Proof state:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
⊢ ∑ i : ZMod N, stdAddChar (t * i) = if t = 0 then ↑N else 0

Tactic:
split_ifs with h

Result:
case pos
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
h : t = 0
⊢ ∑ i : ZMod N, stdAddChar (t * i) = ↑N

case neg
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
h : ¬t = 0
⊢ ∑ i : ZMod N, stdAddChar (t * i) = 0

Proof state:
case neg
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
h : ¬t = 0
⊢ ∑ i : ZMod N, stdAddChar (t * i) = 0

Tactic:
exact sum_eq_zero_of_ne_one (isPrimitive_stdAddChar N h)

Result:
no goals

Proof state:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ∑ x : ZMod N, ∑ x_1 : ZMod N, stdAddChar (-((j + x_1) * x)) • Φ x_1 = ↑N • Φ (-j)

Tactic:
rw [sum_comm]

Result:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ∑ y : ZMod N, ∑ x : ZMod N, stdAddChar (-((j + y) * x)) • Φ y = ↑N • Φ (-j)

Proof state:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j✝ : ZMod N
h1 : ∀ (t : ZMod N), ∑ i : ZMod N, stdAddChar (t * i) = if t = 0 then ↑N else 0
x j : ZMod N
⊢ -(j + x) = 0 ↔ x = -j

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

Result:
no goals

Proof state:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
h1 : ∀ (t : ZMod N), ∑ i : ZMod N, stdAddChar (t * i) = if t = 0 then ↑N else 0
h2 : ∀ (x j : ZMod N), -(j + x) = 0 ↔ x = -j
⊢ ∑ x : ZMod N, (∑ i : ZMod N, stdAddChar (-(j + x) * i)) • Φ x = ↑N • Φ (-j)

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

Result:
no goals

Proof state:
case pos
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
h : t = 0
⊢ ∑ i : ZMod N, stdAddChar (t * i) = ↑N

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

Result:
no goals

Proof state:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
h1 : ∀ (t : ZMod N), ∑ i : ZMod N, stdAddChar (t * i) = if t = 0 then ↑N else 0
⊢ ∑ x : ZMod N, (∑ i : ZMod N, stdAddChar (-(j + x) * i)) • Φ x = ↑N • Φ (-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]

Result:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
h1 : ∀ (t : ZMod N), ∑ i : ZMod N, stdAddChar (t * i) = if t = 0 then ↑N else 0
h2 : ∀ (x j : ZMod N), -(j + x) = 0 ↔ x = -j
⊢ ∑ x : ZMod N, (∑ i : ZMod N, stdAddChar (-(j + x) * i)) • Φ x = ↑N • Φ (-j)