-- Mathlib/NumberTheory/GaussSum.lean
/-- A formula for the product of two Gauss sums with the same additive character. -/
lemma gaussSum_mul {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing R']
    (χ φ : MulChar R R') (ψ : AddChar R R') :
    gaussSum χ ψ * gaussSum φ ψ = ∑ t : R, ∑ x : R, χ x * φ (t - x) * ψ t

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x b : R
x✝ : b ∈ univ
⊢ b - x + x = b

Tactic:
rw [sub_add_cancel]

Result:
no goals

Proof state:
case i_inj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a₁ ∈ univ, ∀ a₂ ∈ univ, a₁ + x = a₂ + x → a₁ = a₂

Tactic:
simp only [mem_univ, add_left_inj, imp_self, forall_const]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x : R, ∑ x_1 : R, χ x * φ x_1 * (ψ x * ψ x_1) = ∑ t : R, ∑ x : R, χ x * φ (t - x) * ψ t

Tactic:
simp only [← ψ.map_add_eq_mul]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x : R, ∑ x_1 : R, χ x * φ x_1 * ψ (x + x_1) = ∑ t : R, ∑ x : R, χ x * φ (t - x) * ψ t

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∑ y : R, χ x * φ y * ψ (x + y) = ∑ y : R, χ x * φ (y - x) * ψ y

Tactic:
rw [sum_bij (fun a _ ↦ a + x)]

Result:
case hi
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, a + x ∈ univ

case i_inj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a₁ ∈ univ, ∀ a₂ ∈ univ, a₁ + x = a₂ + x → a₁ = a₂

case i_surj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ b ∈ univ, ∃ a, ∃ (_ : a ∈ univ), a + x = b

case h
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, χ x * φ a * ψ (x + a) = χ x * φ (a + x - x) * ψ (a + x)

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ i : R, ∑ j : R, χ i * ψ i * (φ j * ψ j) = ∑ t : R, ∑ x : R, χ x * φ (t - x) * ψ t

Tactic:
conv => enter [1, 2, x, 2, x_1]; rw [mul_mul_mul_comm]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x : R, ∑ x_1 : R, χ x * φ x_1 * (ψ x * ψ x_1) = ∑ t : R, ∑ x : R, χ x * φ (t - x) * ψ t

Proof state:
case hi
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, a + x ∈ univ

Tactic:
simp only [mem_univ, forall_true_left, forall_const]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x a : R
x✝ : a ∈ univ
⊢ χ x * φ a * ψ (x + a) = χ x * φ (a + x - x) * ψ (a + x)

Tactic:
rw [add_sub_cancel_right, add_comm]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
sum_eq : ∀ (x : R), ∑ y : R, χ x * φ y * ψ (x + y) = ∑ y : R, χ x * φ (y - x) * ψ y
⊢ ∑ x : R, ∑ x_1 : R, χ x * φ x_1 * ψ (x + x_1) = ∑ t : R, ∑ x : R, χ x * φ (t - x) * ψ t

Tactic:
rw [sum_congr rfl fun x _ ↦ sum_eq x, sum_comm]

Result:
no goals

Proof state:
case h
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, χ x * φ a * ψ (x + a) = χ x * φ (a + x - x) * ψ (a + x)

Tactic:
exact fun a _ ↦ by rw [add_sub_cancel_right, add_comm]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ gaussSum χ ψ * gaussSum φ ψ = ∑ t : R, ∑ x : R, χ x * φ (t - x) * ψ t

Tactic:
rw [gaussSum, gaussSum, sum_mul_sum]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ i : R, ∑ j : R, χ i * ψ i * (φ j * ψ j) = ∑ t : R, ∑ x : R, χ x * φ (t - x) * ψ t

Proof state:
case i_surj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ b ∈ univ, ∃ a, ∃ (_ : a ∈ univ), a + x = b

Tactic:
exact fun b _ ↦ ⟨b - x, mem_univ _, by rw [sub_add_cancel]⟩

Result:
no goals