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 : Finite F
n : ℕ
inst_4 : NeZero n
χ : MulChar F R
μ : R
hχ : χ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx : x ≠ 0
obtain :
  ∀ k < n,
    ∀ (hk : (χ : (a : F) → R) x = μ ^ k),
      ∃ (z : R),
        Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) = z * (μ - 1)
⊢ ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) = z * (μ - 1)

Tactic:
obtain ⟨k, _, hk⟩ := exists_apply_eq_pow hχ hμ hx

Premises used: MulChar.exists_apply_eq_pow
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ : MulChar F R
μ : R
hχ : χ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx : x ≠ 0
k : ℕ
left : k < n
hk : (χ : (a : F) → R) x = μ ^ k
⊢ ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) = z * (μ - 1)

Tactic:
hk ▸ ⟨(Finset.range k).sum (μ ^ ·), ?_, (geom_sum_mul μ k).symm⟩

Premises used: Eq.rec, geom_sum_mul, Finset.range, HPow.hPow, And.intro, Exists.intro, Eq.symm, Finset.sum
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ : MulChar F R
μ : R
hχ : χ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx : x ≠ 0
k : ℕ
left : k < n
hk : (χ : (a : F) → R) x = μ ^ k
refine : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∑ x ∈ range k, μ ^ x)
⊢ ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) = z * (μ - 1)

Tactic:
refine hk ▸ ⟨(Finset.range k).sum (μ ^ ·), ?_, (geom_sum_mul μ k).symm⟩
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ : MulChar F R
μ : R
hχ : χ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx : x ≠ 0
k : ℕ
left : k < n
hk : (χ : (a : F) → R) x = μ ^ k
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∑ x ∈ range k, μ ^ x)

Tactic:
Subalgebra.sum_mem _ fun m _ ↦ Subalgebra.pow_mem _ (self_mem_adjoin_singleton _ μ) _

Premises used: Set.Mem, Algebra.adjoin, Subalgebra.sum_mem, Int, Subalgebra.pow_mem, Singleton.singleton, Algebra.self_mem_adjoin_singleton
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ : MulChar F R
μ : R
hχ : χ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx : x ≠ 0
k : ℕ
left : k < n
hk : (χ : (a : F) → R) x = μ ^ k
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∑ x ∈ range k, μ ^ x)

Tactic:
exact Subalgebra.sum_mem _ fun m _ ↦ Subalgebra.pow_mem _ (self_mem_adjoin_singleton _ μ) _

Premises used: Algebra.adjoin, Subalgebra.sum_mem, Subalgebra.pow_mem, Singleton.singleton, Algebra.self_mem_adjoin_singleton
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
inl :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 0) : R) (1 : R) =
        z * HPow.hPow (β := ℕ) (μ - 1) 2
inr :
  ∀ (hx₀ : x ≠ 0),
    ∃ (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 ∧
      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:
rcases eq_or_ne x 0 with rfl | hx₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
rw :
  HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) *
      HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) 1 : R) (1 : R) =
    0 * HPow.hPow (β := ℕ) (μ - 1) 2
rw₁ :
  HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) * HSub.hSub (α := R) 1 1 =
    0 * HPow.hPow (β := ℕ) (μ - 1) 2
rw₂ : HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) * 0 = 0 * HPow.hPow (β := ℕ) (μ - 1) 2
rw₃ : 0 = 0 * HPow.hPow (β := ℕ) (μ - 1) 2
rw₄ rw₅ : Eq.{u_2 + 1} (α := R) 0 0
⊢ HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) *
      HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 0) : R) (1 : R) =
    0 * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
rw [sub_zero, ψ.map_one, sub_self, mul_zero, zero_mul]

Premises used: MulChar.map_one, sub_self, sub_zero, MulZeroClass.zero_mul, MulZeroClass.mul_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 : Finite F
n : ℕ
inst_4 : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
⊢ ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 0) : R) (1 : R) =
        z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
exact ⟨0, Subalgebra.zero_mem _, by rw [sub_zero, ψ.map_one, sub_self, mul_zero, zero_mul]⟩
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
inr :
  ∀ (hx₀ : Ne.{u_1 + 1} (α := F) 1 0),
    ∃ (z : R),
      Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 1 : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R) =
          z * HPow.hPow (β := ℕ) (μ - 1) 2
inr₁ :
  ∀ (hx₁ : x ≠ 1),
    ∃ (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 ∧
      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:
rcases eq_or_ne x 1 with rfl | hx₁

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
hx₀ : Ne.{u_1 + 1} (α := F) 1 0
rw :
  HSub.hSub (α := R) 1 1 * HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R) =
    0 * HPow.hPow (β := ℕ) (μ - 1) 2
rw₁ :
  0 * HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R) =
    0 * HPow.hPow (β := ℕ) (μ - 1) 2
rw₂ : 0 = 0 * HPow.hPow (β := ℕ) (μ - 1) 2
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) 0 0
⊢ HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 1 : R) (1 : R) *
      HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R) =
    0 * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
rw [χ.map_one, sub_self, zero_mul, zero_mul]

Premises used: MulChar.map_one, sub_self, MulZeroClass.zero_mul
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
hx₀ : Ne.{u_1 + 1} (α := F) 1 0
⊢ ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 1 : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R) =
        z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
exact ⟨0, Subalgebra.zero_mem _, by rw [χ.map_one, sub_self, zero_mul, zero_mul]⟩
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
inr :
  ∀ (z₁ : R) (hz₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z₁)
    (Hz₁ : HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) = z₁ * (μ - 1)),
    ∃ (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 ∧
      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:
obtain ⟨z₁, hz₁, Hz₁⟩ := MulChar.exists_apply_sub_one_eq_mul_sub_one hχ hμ hx₀

Premises used: _private.0.MulChar.exists_apply_sub_one_eq_mul_sub_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 : Finite F
n : ℕ
inst_4 : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
z₁ : R
hz₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z₁
Hz₁ : HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) = z₁ * (μ - 1)
inr :
  ∀ (z₂ : R) (hz₂ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z₂)
    (Hz₂ : HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) = z₂ * (μ - 1)),
    ∃ (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 ∧
      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:
obtain ⟨z₂, hz₂, Hz₂⟩ :=
    MulChar.exists_apply_sub_one_eq_mul_sub_one hψ hμ (sub_ne_zero_of_ne hx₁.symm)

Premises used: _private.0.MulChar.exists_apply_sub_one_eq_mul_sub_one, Ne.symm, sub_ne_zero_of_ne
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
z₁ : R
hz₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z₁
Hz₁ : HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) = z₁ * (μ - 1)
z₂ : R
hz₂ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z₂
Hz₂ : HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) = z₂ * (μ - 1)
inr : ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ z₁ * (μ - 1) * (z₂ * (μ - 1)) = z * ((μ - 1) * (μ - 1))
⊢ ∃ (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:
rewrite [Hz₁, Hz₂, sq]

Premises used: sq
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
z₁ : R
hz₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z₁
Hz₁ : HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) = z₁ * (μ - 1)
z₂ : R
hz₂ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z₂
Hz₂ : HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) = z₂ * (μ - 1)
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ z₁ * (μ - 1) * (z₂ * (μ - 1)) = z * ((μ - 1) * (μ - 1))

Tactic:
⟨z₁ * z₂, Subalgebra.mul_mem _ hz₁ hz₂, mul_mul_mul_comm ..⟩

Premises used: Subalgebra.mul_mem, HMul.hMul, mul_mul_mul_comm, And.intro, Exists.intro
-- 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 : Finite F
n : ℕ
inst_4 : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
z₁ : R
hz₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z₁
Hz₁ : HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) = z₁ * (μ - 1)
z₂ : R
hz₂ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z₂
Hz₂ : HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) = z₂ * (μ - 1)
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ z₁ * (μ - 1) * (z₂ * (μ - 1)) = z * ((μ - 1) * (μ - 1))

Tactic:
exact ⟨z₁ * z₂, Subalgebra.mul_mem _ hz₁ hz₂, mul_mul_mul_comm ..⟩
-- 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 : ℕ
inst_4 : NeZero n
χ φ : MulChar F R
hχ : χ ^ n = 1
hφ : φ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (jacobiSum χ φ)

Tactic:
Subalgebra.sum_mem _ fun _ _ ↦ Subalgebra.mul_mem _
    (MulChar.apply_mem_algebraAdjoin_of_pow_eq_one hχ hμ _)
    (MulChar.apply_mem_algebraAdjoin_of_pow_eq_one hφ hμ _)

Premises used: Subalgebra.mul_mem, MulChar.apply_mem_algebraAdjoin_of_pow_eq_one, Set.Mem, HSub.hSub, Algebra.adjoin, Subalgebra.sum_mem, jacobiSum, Int, Singleton.singleton, 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
hn' : n ∣ Fintype.card F - 1
hμ : IsPrimitiveRoot μ n
obtain :
  ∀ (q : ℕ) (hq : Fintype.card F - 1 = n * q),
    ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
obtain ⟨q, hq⟩ := hn'
-- 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 - 1 = n * q
⊢ Fintype.card F = n * q + 1

Tactic:
rw [Nat.sub_eq_iff_eq_add NeZero.one_le] at hq

Premises used: NeZero.one_le, Nat.sub_eq_iff_eq_add
-- 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
obtain :
  ∀ (z₁ : R) (hz₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z₁) (Hz₁ : (↑n : R) = z₁ * HPow.hPow (β := ℕ) (μ - 1) 2),
    ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
obtain ⟨z₁, hz₁, Hz₁⟩ := hμ.self_sub_one_pow_dvd_order hn

Premises used: IsPrimitiveRoot.self_sub_one_pow_dvd_order
-- 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
pos :
  ∀ (hχ₀ : χ = 1),
    ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg :
  ∀ (hχ₀ : ¬χ = 1),
    ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
by_cases hχ₀ : χ = 1
-- 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
pos :
  ∀ (hψ₀ : ψ = 1),
    ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg :
  ∀ (hψ₀ : ¬ψ = 1),
    ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
by_cases hψ₀ : ψ = 1
-- 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
pos :
  ∀ (hψ₀ : ψ = 1),
    ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg :
  ∀ (hψ₀ : ¬ψ = 1),
    ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
by_cases hψ₀ : ψ = 1
-- 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 :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HSub.hSub (α := R) (↑(Fintype.card F) : R) 2 = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
rw [hχ₀, hψ₀, jacobiSum_one_one]

Premises used: jacobiSum_one_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
⊢ ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HSub.hSub (α := R) (↑(Fintype.card F) : R) 2 = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
⟨q * z₁, Subalgebra.mul_mem _ (Subalgebra.natCast_mem _ q) hz₁, ?_⟩

Premises used: Subalgebra.mul_mem, HMul.hMul, Nat.cast, And.intro, Exists.intro, 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
pos : HSub.hSub (α := R) (↑(Fintype.card F) : R) 2 = -1 + (↑q : R) * z₁ * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HSub.hSub (α := R) (↑(Fintype.card F) : R) 2 = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
refine ⟨q * z₁, Subalgebra.mul_mem _ (Subalgebra.natCast_mem _ q) hz₁, ?_⟩
-- 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 : z₁ * HPow.hPow (β := ℕ) (μ - 1) 2 * (↑q : R) + (↑1 : R) - 2 = -1 + (↑q : R) * z₁ * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ HSub.hSub (α := R) (↑(Fintype.card F) : R) 2 = -1 + (↑q : R) * z₁ * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
rw [hq, Nat.cast_add, Nat.cast_mul, Hz₁]

Premises used: Nat.cast_add, Nat.cast_mul
-- 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₁ * HPow.hPow (β := ℕ) (μ - 1) 2 * (↑q : R) + (↑1 : R) - 2 = -1 + (↑q : R) * z₁ * HPow.hPow (β := ℕ) (μ - 1) 2

Tactic:
ring
-- 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
neg : 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 _, ?_⟩