awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [sub_zero, ψ.map_one, sub_self, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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
have rw₁ : HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) * HSub.hSub (α := R) 1 1 =
  0 * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: rw [sub_zero, ψ.map_one, sub_self, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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
have rw₂ : HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) * 0 = 0 * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: rw [sub_zero, ψ.map_one, sub_self, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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
have rw₃ : 0 = 0 * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: rw [sub_zero, ψ.map_one, sub_self, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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
have rw₄ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [sub_zero, ψ.map_one, sub_self, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases eq_or_ne x 1 with rfl | hx₁
Cleared hypotheses: x, hx₀
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases eq_or_ne x 1 with rfl | hx₁
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [χ.map_one, sub_self, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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
have rw₁ : 0 * 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]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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
have rw₂ : 0 = 0 * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: rw [χ.map_one, sub_self, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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
have rw₃ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [χ.map_one, sub_self, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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),
    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
have 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
Tactic: obtain ⟨z₁, hz₁, Hz₁⟩ := MulChar.exists_apply_sub_one_eq_mul_sub_one hχ hμ hx₀
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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),
    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
have 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
Tactic: obtain ⟨z₂, hz₂, Hz₂⟩ :=
    MulChar.exists_apply_sub_one_eq_mul_sub_one hψ hμ (sub_ne_zero_of_ne hx₁.symm)
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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 ∧
      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
have inr : ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ z₁ * (μ - 1) * (z₂ * (μ - 1)) = z * ((μ - 1) * (μ - 1))
Tactic: rewrite [Hz₁, Hz₂, sq]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have obtain : ∀ (q : ℕ) (hq : Fintype.card F - 1 = n * q),
  ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: obtain ⟨q, hq⟩ := hn'
Cleared hypotheses: hn'
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
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
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have hq₁ : Fintype.card F = n * q + 1
Tactic: rw [Nat.sub_eq_iff_eq_add NeZero.one_le] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have 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
Tactic: obtain ⟨z₁, hz₁, Hz₁⟩ := hμ.self_sub_one_pow_dvd_order hn
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have pos : ∀ (hχ₀ : χ = 1),
  ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: by_cases hχ₀ : χ = 1
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have neg : ∀ (hχ₀ : ¬χ = 1),
  ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: by_cases hχ₀ : χ = 1
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have pos : ∀ (hψ₀ : ψ = 1),
  ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: by_cases hψ₀ : ψ = 1
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have neg : ∀ (hψ₀ : ¬ψ = 1),
  ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: by_cases hψ₀ : ψ = 1
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have pos : ∀ (hψ₀ : ψ = 1),
  ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: by_cases hψ₀ : ψ = 1
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have neg : ∀ (hψ₀ : ¬ψ = 1),
  ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: by_cases hψ₀ : ψ = 1
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
have pos : ∃ (z : R),
  Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
    HSub.hSub (α := R) (↑(Fintype.card F) : R) 2 = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: rw [hχ₀, hψ₀, jacobiSum_one_one]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
have pos : HSub.hSub (α := R) (↑(Fintype.card F) : R) 2 = -1 + (↑q : R) * z₁ * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: refine ⟨q * z₁, Subalgebra.mul_mem _ (Subalgebra.natCast_mem _ q) hz₁, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ HSub.hSub (α := R) (↑(Fintype.card F) : R) 2 = -1 + (↑q : R) * z₁ * HPow.hPow (β := ℕ) (μ - 1) 2
have pos : z₁ * HPow.hPow (β := ℕ) (μ - 1) 2 * (↑q : R) + (↑1 : R) - 2 = -1 + (↑q : R) * z₁ * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: rw [hq, Nat.cast_add, Nat.cast_mul, Hz₁]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
have neg : jacobiSum χ ψ = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: refine ⟨0, Subalgebra.zero_mem _, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ jacobiSum χ ψ = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2
have neg : jacobiSum 1 ψ = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: rw [hχ₀, jacobiSum_one_nontrivial hψ₀, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ jacobiSum χ ψ = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2
have neg₁ : -1 = -1 + 0 * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: rw [hχ₀, jacobiSum_one_nontrivial hψ₀, zero_mul, add_zero]