awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : jacobiSum 1 ψ = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2
neg₁ : -1 = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2
neg₂ : -1 = HAdd.hAdd (α := R) (-1) 0
neg₃ neg₄ : Eq.{u_2 + 1} (α := R) (-1) (-1)
⊢ jacobiSum χ ψ = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
rw [hχ₀, jacobiSum_one_nontrivial hψ₀, zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, jacobiSum_one_nontrivial, add_zero
-- 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
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
⟨0, Subalgebra.zero_mem _, ?_⟩

Premises used: Subalgebra.zero_mem, And.intro, Exists.intro, OfNat.ofNat
-- 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
pos : jacobiSum χ ψ = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
refine ⟨0, Subalgebra.zero_mem _, ?_⟩
-- 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
pos : jacobiSum ψ χ = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2
pos₁ : jacobiSum 1 χ = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2
pos₂ : -1 = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2
pos₃ : -1 = HAdd.hAdd (α := R) (-1) 0
pos₄ pos₅ : Eq.{u_2 + 1} (α := R) (-1) (-1)
⊢ jacobiSum χ ψ = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
rw [jacobiSum_comm, hψ₀, jacobiSum_one_nontrivial hχ₀, zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, jacobiSum_one_nontrivial, jacobiSum_comm, add_zero
-- 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) 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
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
rw [jacobiSum_eq_aux, MulChar.sum_eq_zero_of_ne_one hχ₀, MulChar.sum_eq_zero_of_ne_one hψ₀, hq]

Premises used: _private.0.jacobiSum_eq_aux, MulChar.sum_eq_zero_of_ne_one
-- 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
⊢ n ≠ 0

Tactic:
lia
-- 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
⊢ NeZero n

Tactic:
have : NeZero n := ⟨by lia⟩
-- 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
this : NeZero n
⊢ ∀ (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

Tactic:
have H := MulChar.exists_apply_sub_one_mul_apply_sub_one hχ hψ hμ
-- 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
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
⊢ ∀ (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

Tactic:
have Hcs x := (H x).choose_spec
-- 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
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

Tactic:
⟨-q * z₁ + ∑ x ∈ (univ \ {0, 1} : Finset F), (H x).choose, ?_, ?_⟩

Premises used: HMul.hMul, Finset.univ, Insert.insert, Nat.cast, SDiff.sdiff, HAdd.hAdd, And.intro, Exists.intro, Exists.choose, Singleton.singleton, OfNat.ofNat, Finset.sum, Neg.neg
-- 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
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
neg :
  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₁ :
  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 ∧
      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

Tactic:
refine ⟨-q * z₁ + ∑ x ∈ (univ \ {0, 1} : Finset F), (H x).choose, ?_, ?_⟩
-- 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
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))

Tactic:
Subalgebra.add_mem _ (Subalgebra.mul_mem _ (Subalgebra.neg_mem _ ?_) hz₁) ?_

Premises used: Subalgebra.mul_mem, Subalgebra.add_mem, Subalgebra.neg_mem
-- 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
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)

Tactic:
Subalgebra.natCast_mem ..

Premises used: Set.Mem, Subalgebra.natCast_mem
-- 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
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)

Tactic:
exact Subalgebra.natCast_mem ..

Premises used: Subalgebra.natCast_mem
-- 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
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) ℤ[μ]
    (∑ 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))

Tactic:
Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1

Premises used: Set.Mem, Subalgebra.sum_mem, And.left
-- 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
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) ℤ[μ]
    (∑ 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))

Tactic:
exact Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1

Premises used: Subalgebra.sum_mem, And.left