-- Mathlib/NumberTheory/JacobiSum/Basic.lean
private lemma jacobiSum_eq_aux (χ ψ : MulChar F R) :
    jacobiSum χ ψ = ∑ x : F, χ x + ∑ x : F, ψ x - Fintype.card F +
                      ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
x : F
x✝ y✝ : R
⊢ x✝ * y✝ = x✝ + y✝ - 1 + (x✝ - 1) * (y✝ - 1)

Tactic:
ring

Result:
no goals

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F, (χ x + ψ (1 - x) - 1 + (χ x - 1) * (ψ (1 - x) - 1)) =
    ∑ x : F, χ x + ∑ x : F, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
rw [sum_add_distrib, sum_sub_distrib, sum_add_distrib]

Result:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F, χ x + ∑ x : F, ψ (1 - x) - ∑ x : F, 1 + ∑ x : F, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x : F, χ x + ∑ x : F, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F, χ x + ∑ i : F, ψ i - ∑ x : F, 1 + (∑ x : F, (χ x - 1) * (ψ (1 - x) - 1) - 0) =
    ∑ x : F, χ x + ∑ x : F, ψ x - ∑ x : F, 1 +
      (∑ x : F, (χ x - 1) * (ψ (1 - x) - 1) - ∑ x ∈ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1))

Tactic:
congr

Result:
case e_a.e_a
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ 0 = ∑ x ∈ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
x : F
⊢ ∀ (x y : R), x * y = x + y - 1 + (x - 1) * (y - 1)

Tactic:
intros

Result:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
x : F
x✝ y✝ : R
⊢ x✝ * y✝ = x✝ + y✝ - 1 + (x✝ - 1) * (y✝ - 1)

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F, χ x + ∑ x : F, ψ ((Equiv.subLeft 1) x) - ∑ x : F, 1 + ∑ x : F, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x : F, χ x + ∑ x : F, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
rw [(Equiv.subLeft 1).sum_comp ψ, Fintype.card_eq_sum_ones, Nat.cast_sum, Nat.cast_one,
  sum_sdiff_eq_sub (subset_univ _), ← sub_zero (_ - _ + _), add_sub_assoc]

Result:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F, χ x + ∑ i : F, ψ i - ∑ x : F, 1 + (∑ x : F, (χ x - 1) * (ψ (1 - x) - 1) - 0) =
    ∑ x : F, χ x + ∑ x : F, ψ x - ∑ x : F, 1 +
      (∑ x : F, (χ x - 1) * (ψ (1 - x) - 1) - ∑ x ∈ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1))

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F, χ x * ψ (1 - x) =
    ∑ x : F, χ x + ∑ x : F, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
conv =>
  enter [1, 2, x]
  rw [show ∀ x y : R, x * y = x + y - 1 + (x - 1) * (y - 1) by intros; ring]

Result:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F, (χ x + ψ (1 - x) - 1 + (χ x - 1) * (ψ (1 - x) - 1)) =
    ∑ x : F, χ x + ∑ x : F, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F, χ x + ∑ x : F, ψ (1 - x) - ∑ x : F, 1 + ∑ x : F, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x : F, χ x + ∑ x : F, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
conv => enter [1, 1, 1, 2, 2, x]; rw [← Equiv.subLeft_apply 1]

Result:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F, χ x + ∑ x : F, ψ ((Equiv.subLeft 1) x) - ∑ x : F, 1 + ∑ x : F, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x : F, χ x + ∑ x : F, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ jacobiSum χ ψ = ∑ x : F, χ x + ∑ x : F, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
rw [jacobiSum]

Result:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F, χ x * ψ (1 - x) =
    ∑ x : F, χ x + ∑ x : F, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Proof state:
case e_a.e_a
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ 0 = ∑ x ∈ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
rw [sum_pair zero_ne_one, sub_zero, ψ.map_one, χ.map_one, sub_self, mul_zero, zero_mul, add_zero]

Result:
no goals