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
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
h :
  ∀ (x : F),
    HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
      HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
| 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

Tactic:
enter [1, 2, 2, x]
-- 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
x : F
h :
  ⋯.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
| HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
    HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)

Tactic:
rw [(Hcs x).2]

Premises used: And.right
-- 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
h :
  ∀ (x : F),
    ⋯.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

Tactic:
enter [1, 2, 2, x]; rw [(Hcs x).2]
-- 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 :
  HAdd.hAdd (α := R) 0 0 - (↑(n * q + 1) : 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) *
          HPow.hPow (β := ℕ) (μ - 1) 2 =
    -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
⊢ 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

Tactic:
conv => enter [1, 2, 2, x]; rw [(Hcs x).2]
-- 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
⊢ HAdd.hAdd (α := R) 0 0 - (z₁ * HPow.hPow (β := ℕ) (μ - 1) 2 * (↑q : R) + (↑1 : R)) +
      (∑ i ∈ univ \ {0, 1},
          ⋯.choose (p := fun (z : R) ↦
            Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
              HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) i : R) (1 : R) *
                  HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - i) : R) (1 : R) =
                z * HPow.hPow (β := ℕ) (μ - 1) 2)) *
        HPow.hPow (β := ℕ) (μ - 1) 2 =
    -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

Tactic:
ring
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n : ℕ
hn₂ : Nat.succ 0 < orderOf χ
⊢ gaussSum χ ψ ^ Nat.succ 0 = gaussSum (χ ^ Nat.succ 0) ψ * ∏ j ∈ Ico 1 (Nat.succ 0), jacobiSum χ (χ ^ j)

Tactic:
simp only [pow_one, le_refl, Ico_eq_empty_of_le, prod_empty, mul_one]

Premises used: Finset.prod_empty, le_refl, Finset.Ico_eq_empty_of_le, pow_one, mul_one
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n_1 n : ℕ
hn : Nat.succ 0 ≤ n
ih : ∀ (hn₂ : n < orderOf χ), gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
hn₂ : n + 1 < orderOf χ
⊢ gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)

Tactic:
specialize ih <| lt_trans (Nat.lt_succ_self n) hn₂

Premises used: lt_trans, Nat.lt_succ_self
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n_1 n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
ih : gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
⊢ χ * χ ^ n ≠ 1

Tactic:
have hχn : χ * (χ ^ n) ≠ 1 :=
          pow_succ' χ n ▸ pow_ne_one_of_lt_orderOf n.add_one_ne_zero hn₂
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n_1 n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
ih : gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
hχn : χ * χ ^ n ≠ 1
rw : gaussSum χ ψ * gaussSum (χ ^ n) ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
rw₁ : gaussSum (χ * χ ^ n) ψ * jacobiSum χ (χ ^ n) = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
rw₂ : jacobiSum χ (χ ^ n) * gaussSum (χ * χ ^ n) ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
rw₃ rw₄ : jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
⊢ gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ

Tactic:
rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ']

Premises used: jacobiSum_mul_nontrivial, mul_comm, pow_succ'
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n_1 n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
ih : gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
⊢ gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ

Tactic:
have gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ =
            jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ := by
        have hχn : χ * (χ ^ n) ≠ 1 :=
          pow_succ' χ n ▸ pow_ne_one_of_lt_orderOf n.add_one_ne_zero hn₂
        rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ']
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n_1 n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
ih : gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
⊢ gaussSum χ ψ ^ n * gaussSum χ ψ = (gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)) * gaussSum χ ψ

Tactic:
apply_fun (· * gaussSum χ ψ) at ih

Premises used: HMul.hMul, gaussSum
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n_1 n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
ih : gaussSum χ ψ ^ n * gaussSum χ ψ = (gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)) * gaussSum χ ψ
⊢ gaussSum χ ψ ^ (n + 1) = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)

Tactic:
rw [mul_right_comm, ← pow_succ, gauss_rw] at ih

Premises used: pow_succ, mul_right_comm
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n_1 n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
ih : gaussSum χ ψ ^ (n + 1) = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
succ :
  jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j) =
    gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
succ₁ :
  jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j) =
    gaussSum (χ ^ (n + 1)) ψ * ((∏ k ∈ Ico (Nat.succ 0) n, jacobiSum χ (χ ^ k)) * jacobiSum χ (χ ^ n))
succ₂ :
  (gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)) * jacobiSum χ (χ ^ n) =
    gaussSum (χ ^ (n + 1)) ψ * ((∏ k ∈ Ico (Nat.succ 0) n, jacobiSum χ (χ ^ k)) * jacobiSum χ (χ ^ n))
succ₃ succ₄ :
  gaussSum (χ ^ (n + 1)) ψ * ((∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)) * jacobiSum χ (χ ^ n)) =
    gaussSum (χ ^ (n + 1)) ψ * ((∏ k ∈ Ico (Nat.succ 0) n, jacobiSum χ (χ ^ k)) * jacobiSum χ (χ ^ n))
⊢ gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)

Tactic:
rw [ih, Finset.prod_Ico_succ_top hn, mul_rotate, mul_assoc]

Premises used: mul_assoc, Finset.prod_Ico_succ_top, mul_rotate
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n : ℕ
hn₁ : 0 < n
hn₂ : n < orderOf χ
base :
  ∀ (hn₂ : Nat.succ 0 < orderOf χ),
    gaussSum χ ψ ^ Nat.succ 0 = gaussSum (χ ^ Nat.succ 0) ψ * ∏ j ∈ Ico 1 (Nat.succ 0), jacobiSum χ (χ ^ j)
succ :
  ∀ (n : ℕ) (hn : Nat.succ 0 ≤ n)
    (ih : ∀ (hn₂ : n < orderOf χ), gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j))
    (hn₂ : n + 1 < orderOf χ),
    gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
⊢ gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)

Tactic:
induction n, hn₁ using Nat.le_induction with
  | base => simp only [pow_one, le_refl, Ico_eq_empty_of_le, prod_empty, mul_one]
  | succ n hn ih =>
      specialize ih <| lt_trans (Nat.lt_succ_self n) hn₂
      have gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ =
            jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ := by
        have hχn : χ * (χ ^ n) ≠ 1 :=
          pow_succ' χ n ▸ pow_ne_one_of_lt_orderOf n.add_one_ne_zero hn₂
        rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ']
      apply_fun (· * gaussSum χ ψ) at ih
      rw [mul_right_comm, ← pow_succ, gauss_rw] at ih
      rw [ih, Finset.prod_Ico_succ_top hn, mul_rotate, mul_assoc]

Premises used: Finset.prod_empty, le_refl, HMul.hMul, pow_succ, mul_assoc, lt_trans, Nat.lt_succ_self, Finset.Ico_eq_empty_of_le, mul_right_comm, pow_one, gaussSum, mul_one, mul_rotate
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
⊢ 0 < orderOf χ - 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
⊢ orderOf χ - 1 < orderOf χ

Tactic:
lia
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
⊢ gaussSum χ ψ ^ (orderOf χ - 1) = gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j)

Tactic:
have := gaussSum_pow_eq_prod_jacobiSum_aux χ ψ (n := orderOf χ - 1) (by lia) (by lia)
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
this :
  gaussSum χ ψ ^ (orderOf χ - 1) = gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j)
⊢ gaussSum χ ψ * gaussSum χ ψ ^ (orderOf χ - 1) =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))

Tactic:
apply_fun (gaussSum χ ψ * ·) at this

Premises used: HMul.hMul, gaussSum
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
this :
  gaussSum χ ψ ^ (orderOf χ - 1 + 1) =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
⊢ 0 < orderOf χ

Tactic:
lia
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
this :
  gaussSum χ ψ * gaussSum χ ψ ^ (orderOf χ - 1) =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
⊢ gaussSum χ ψ ^ orderOf χ =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))

Tactic:
rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos (by lia)] at this

Premises used: Nat.sub_one_add_one_eq_of_pos, pow_succ'
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
this :
  gaussSum χ ψ ^ orderOf χ =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
⊢ χ ≠ 1

Tactic:
have hχ₁ : χ ≠ 1 :=
    fun h ↦ ((orderOf_one (G := MulChar F R) ▸ h ▸ hχ).trans_lt Nat.one_lt_two).false