-- Mathlib/NumberTheory/GaussSum.lean
theorem gaussSum_mul_gaussSum_eq_card {χ : MulChar R R'} (hχ : χ ≠ 1) {ψ : AddChar R R'}
    (hψ : IsPrimitive ψ) :
    gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = Fintype.card R

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x : R, ∑ i : R, χ i * ψ i * (χ x⁻¹ * ψ (-x)) = ↑(Fintype.card R)

Tactic:
conv =>
  enter [1, 2, x, 2, y]
  rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]

Result:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x : R, ∑ y : R, χ (y * x⁻¹) * ψ (y - x) = ↑(Fintype.card R)

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ (∑ x : R, if x = 1 then χ x * ↑(Fintype.card R) else 0) = ↑(Fintype.card R)

Tactic:
rw [Finset.sum_ite_eq' Finset.univ (1 : R)]

Result:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ (if 1 ∈ Finset.univ then χ 1 * ↑(Fintype.card R) else 0) = ↑(Fintype.card R)

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ y : R, ∑ x : R, χ y * ψ (x * (y - 1)) = ↑(Fintype.card R)

Tactic:
simp_rw [← Finset.mul_sum, sum_mulShift _ hψ, sub_eq_zero, apply_ite, Nat.cast_zero, mul_zero]

Result:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ (∑ x : R, if x = 1 then χ x * ↑(Fintype.card R) else 0) = ↑(Fintype.card R)

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ y : R, ∑ x : R, χ y * ψ (x * (y - 1)) = ↑(Fintype.card R)

Tactic:
classical simp_rw [← Finset.mul_sum, sum_mulShift _ hψ, sub_eq_zero, apply_ite, Nat.cast_zero, mul_zero]
rw [Finset.sum_ite_eq' Finset.univ (1 : R)]
simp only [Finset.mem_univ, map_one, one_mul, if_true]

Result:
no goals

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card R)

Tactic:
simp only [gaussSum, AddChar.inv_apply, Finset.sum_mul, Finset.mul_sum, MulChar.inv_apply']

Result:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x : R, ∑ i : R, χ i * ψ i * (χ x⁻¹ * ψ (-x)) = ↑(Fintype.card R)

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x : R, ∑ y : R, χ (y * x⁻¹) * ψ (y - x) = ↑(Fintype.card R)

Tactic:
simp_rw [gaussSum_mul_aux hχ ψ]

Result:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x : R, ∑ c : R, χ c * ψ (x * (c - 1)) = ↑(Fintype.card R)

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x : R, ∑ c : R, χ c * ψ (x * (c - 1)) = ↑(Fintype.card R)

Tactic:
rw [Finset.sum_comm]

Result:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ y : R, ∑ x : R, χ y * ψ (x * (y - 1)) = ↑(Fintype.card R)

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ (if 1 ∈ Finset.univ then χ 1 * ↑(Fintype.card R) else 0) = ↑(Fintype.card R)

Tactic:
simp only [Finset.mem_univ, map_one, one_mul, if_true]

Result:
no goals