-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Field F
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z₁
Hz₁ : (↑n : R) = z₁ * HPow.hPow (β := ℕ) (μ - 1) 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
neg :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₁ :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) 0 (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₂ :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) 0 0 - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₃ neg₄ neg₅ :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) 0 0 - (↑(n * q + 1) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₆ :
  ∀ (this : NeZero n),
    ∃ (z : R),
      Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
        HAdd.hAdd (α := R) 0 0 - (↑(n * q + 1) : R) +
            ∑ x ∈ univ \ {0, 1},
              HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
          -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₇ :
  ∀ (this : NeZero n)
    (H :
      ∀ (x : F),
        ∃ (z : R),
          Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
              z * HPow.hPow (β := ℕ) (μ - 1) 2),
    ∃ (z : R),
      Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
        HAdd.hAdd (α := R) 0 0 - (↑(n * q + 1) : R) +
            ∑ x ∈ univ \ {0, 1},
              HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
          -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₈ :
  ∀ (this : NeZero n)
    (H :
      ∀ (x : F),
        ∃ (z : R),
          Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
              z * HPow.hPow (β := ℕ) (μ - 1) 2)
    (Hcs :
      ∀ (x : F),
        Membership.mem (γ := Subalgebra ℤ R) ℤ[μ]
            (⋯.choose (p := fun (z : R) ↦
              Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
                HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                    HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
                  z * HPow.hPow (β := ℕ) (μ - 1) 2)) ∧
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
            ⋯.choose (p := fun (z : R) ↦
                Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
                  HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                      HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
                    z * HPow.hPow (β := ℕ) (μ - 1) 2) *
              HPow.hPow (β := ℕ) (μ - 1) 2),
    ∃ (z : R),
      Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
        HAdd.hAdd (α := R) 0 0 - (↑(n * q + 1) : R) +
            ∑ x ∈ univ \ {0, 1},
              HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
          -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₉ :
  ∀ (this : NeZero n)
    (H :
      ∀ (x : F),
        ∃ (z : R),
          Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
              z * HPow.hPow (β := ℕ) (μ - 1) 2)
    (Hcs :
      ∀ (x : F),
        Membership.mem (γ := Subalgebra ℤ R) ℤ[μ]
            (⋯.choose (p := fun (z : R) ↦
              Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
                HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                    HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
                  z * HPow.hPow (β := ℕ) (μ - 1) 2)) ∧
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
            ⋯.choose (p := fun (z : R) ↦
                Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
                  HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                      HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
                    z * HPow.hPow (β := ℕ) (μ - 1) 2) *
              HPow.hPow (β := ℕ) (μ - 1) 2),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ]
      (-(↑q : R) * z₁ +
        ∑ x ∈ univ \ {0, 1},
          ⋯.choose (p := fun (z : R) ↦
            Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
              HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                  HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
                z * HPow.hPow (β := ℕ) (μ - 1) 2))
neg₁₀ neg₁₁ :
  ∀ (this : NeZero n)
    (H :
      ∀ (x : F),
        ∃ (z : R),
          Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
              z * HPow.hPow (β := ℕ) (μ - 1) 2)
    (Hcs :
      ∀ (x : F),
        Membership.mem (γ := Subalgebra ℤ R) ℤ[μ]
            (⋯.choose (p := fun (z : R) ↦
              Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
                HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                    HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
                  z * HPow.hPow (β := ℕ) (μ - 1) 2)) ∧
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
            ⋯.choose (p := fun (z : R) ↦
                Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
                  HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                      HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
                    z * HPow.hPow (β := ℕ) (μ - 1) 2) *
              HPow.hPow (β := ℕ) (μ - 1) 2),
    HAdd.hAdd (α := R) 0 0 - (↑(n * q + 1) : R) +
        ∑ x ∈ univ \ {0, 1},
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
      -1 +
        (-(↑q : R) * z₁ +
            ∑ x ∈ univ \ {0, 1},
              ⋯.choose (p := fun (z : R) ↦
                Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
                  HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
                      HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
                    z * HPow.hPow (β := ℕ) (μ - 1) 2)) *
          HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
classical
    rw [jacobiSum_eq_aux, MulChar.sum_eq_zero_of_ne_one hχ₀, MulChar.sum_eq_zero_of_ne_one hψ₀, hq]
    have : NeZero n := ⟨by lia⟩
    have H := MulChar.exists_apply_sub_one_mul_apply_sub_one hχ hψ hμ
    have Hcs x := (H x).choose_spec
    refine ⟨-q * z₁ + ∑ x ∈ (univ \ {0, 1} : Finset F), (H x).choose, ?_, ?_⟩
    · refine Subalgebra.add_mem _ (Subalgebra.mul_mem _ (Subalgebra.neg_mem _ ?_) hz₁) ?_
      · exact Subalgebra.natCast_mem ..
      · exact Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1
    · conv => enter [1, 2, 2, x]; rw [(Hcs x).2]
      rw [← Finset.sum_mul, Nat.cast_add, Nat.cast_mul, Hz₁]
      ring

Premises used: Subalgebra.mul_mem, Subalgebra.add_mem, _private.0.jacobiSum_eq_aux, Subalgebra.neg_mem, Nat.cast_add, Nat.cast_mul, Subalgebra.natCast_mem, MulChar.sum_eq_zero_of_ne_one, Finset.sum_mul