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 : 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 - (↑(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
have neg : HAdd.hAdd (α := R) 0 0 - (↑(n * q + 1) : R) +
    ∑ x ∈ univ \ {0, 1},
      sorry.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},
          sorry.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]
-- 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 : ∃ (z : R),
  Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
    HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
        ∑ x ∈ univ \ {0, 1},
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
      -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: classical
    rw [jacobiSum_eq_aux, MulChar.sum_eq_zero_of_ne_one hχ₀, MulChar.sum_eq_zero_of_ne_one hψ₀, hq]
    have : NeZero n := ⟨by lia⟩
    have H := MulChar.exists_apply_sub_one_mul_apply_sub_one hχ hψ hμ
    have Hcs x := (H x).choose_spec
    refine ⟨-q * z₁ + ∑ x ∈ (univ \ {0, 1} : Finset F), (H x).choose, ?_, ?_⟩
    · refine Subalgebra.add_mem _ (Subalgebra.mul_mem _ (Subalgebra.neg_mem _ ?_) hz₁) ?_
      · exact Subalgebra.natCast_mem ..
      · exact Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1
    · conv => enter [1, 2, 2, x]; rw [(Hcs x).2]
      rw [← Finset.sum_mul, Nat.cast_add, Nat.cast_mul, Hz₁]
      ring
-- 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 :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have neg₁ : ∃ (z : R),
  Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
    HAdd.hAdd (α := R) 0 (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
        ∑ x ∈ univ \ {0, 1},
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
      -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: classical
    rw [jacobiSum_eq_aux, MulChar.sum_eq_zero_of_ne_one hχ₀, MulChar.sum_eq_zero_of_ne_one hψ₀, hq]
    have : NeZero n := ⟨by lia⟩
    have H := MulChar.exists_apply_sub_one_mul_apply_sub_one hχ hψ hμ
    have Hcs x := (H x).choose_spec
    refine ⟨-q * z₁ + ∑ x ∈ (univ \ {0, 1} : Finset F), (H x).choose, ?_, ?_⟩
    · refine Subalgebra.add_mem _ (Subalgebra.mul_mem _ (Subalgebra.neg_mem _ ?_) hz₁) ?_
      · exact Subalgebra.natCast_mem ..
      · exact Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1
    · conv => enter [1, 2, 2, x]; rw [(Hcs x).2]
      rw [← Finset.sum_mul, Nat.cast_add, Nat.cast_mul, Hz₁]
      ring
-- 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 :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₁ :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) 0 (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have neg₂ : ∃ (z : R),
  Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
    HAdd.hAdd (α := R) 0 0 - (↑(Fintype.card F) : R) +
        ∑ x ∈ univ \ {0, 1},
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
      -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: classical
    rw [jacobiSum_eq_aux, MulChar.sum_eq_zero_of_ne_one hχ₀, MulChar.sum_eq_zero_of_ne_one hψ₀, hq]
    have : NeZero n := ⟨by lia⟩
    have H := MulChar.exists_apply_sub_one_mul_apply_sub_one hχ hψ hμ
    have Hcs x := (H x).choose_spec
    refine ⟨-q * z₁ + ∑ x ∈ (univ \ {0, 1} : Finset F), (H x).choose, ?_, ?_⟩
    · refine Subalgebra.add_mem _ (Subalgebra.mul_mem _ (Subalgebra.neg_mem _ ?_) hz₁) ?_
      · exact Subalgebra.natCast_mem ..
      · exact Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1
    · conv => enter [1, 2, 2, x]; rw [(Hcs x).2]
      rw [← Finset.sum_mul, Nat.cast_add, Nat.cast_mul, Hz₁]
      ring
-- 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 :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₁ :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) 0 (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₂ :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) 0 0 - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have 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
Tactic: classical
    rw [jacobiSum_eq_aux, MulChar.sum_eq_zero_of_ne_one hχ₀, MulChar.sum_eq_zero_of_ne_one hψ₀, hq]
    have : NeZero n := ⟨by lia⟩
    have H := MulChar.exists_apply_sub_one_mul_apply_sub_one hχ hψ hμ
    have Hcs x := (H x).choose_spec
    refine ⟨-q * z₁ + ∑ x ∈ (univ \ {0, 1} : Finset F), (H x).choose, ?_, ?_⟩
    · refine Subalgebra.add_mem _ (Subalgebra.mul_mem _ (Subalgebra.neg_mem _ ?_) hz₁) ?_
      · exact Subalgebra.natCast_mem ..
      · exact Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1
    · conv => enter [1, 2, 2, x]; rw [(Hcs x).2]
      rw [← Finset.sum_mul, Nat.cast_add, Nat.cast_mul, Hz₁]
      ring
-- 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 :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₁ :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) 0 (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₂ :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) 0 0 - (↑(Fintype.card F) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
neg₃ neg₄ neg₅ :
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) 0 0 - (↑(n * q + 1) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
⊢ ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ jacobiSum χ ψ = -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
have neg₆ : ∀ (this : NeZero n),
  ∃ (z : R),
    Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧
      HAdd.hAdd (α := R) 0 0 - (↑(n * q + 1) : R) +
          ∑ x ∈ univ \ {0, 1},
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
              HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
        -1 + z * HPow.hPow (β := ℕ) (μ - 1) 2
Tactic: classical
    rw [jacobiSum_eq_aux, MulChar.sum_eq_zero_of_ne_one hχ₀, MulChar.sum_eq_zero_of_ne_one hψ₀, hq]
    have : NeZero n := ⟨by lia⟩
    have H := MulChar.exists_apply_sub_one_mul_apply_sub_one hχ hψ hμ
    have Hcs x := (H x).choose_spec
    refine ⟨-q * z₁ + ∑ x ∈ (univ \ {0, 1} : Finset F), (H x).choose, ?_, ?_⟩
    · refine Subalgebra.add_mem _ (Subalgebra.mul_mem _ (Subalgebra.neg_mem _ ?_) hz₁) ?_
      · exact Subalgebra.natCast_mem ..
      · exact Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1
    · conv => enter [1, 2, 2, x]; rw [(Hcs x).2]
      rw [← Finset.sum_mul, Nat.cast_add, Nat.cast_mul, Hz₁]
      ring
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
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 + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
have ih₁ : gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
Tactic: specialize ih <| lt_trans (Nat.lt_succ_self n) hn₂
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
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)) ψ
have hχn : χ * χ ^ n ≠ 1
Tactic: have hχn : χ * (χ ^ n) ≠ 1 :=
          pow_succ' χ n ▸ pow_ne_one_of_lt_orderOf n.add_one_ne_zero hn₂
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
have rw : gaussSum χ ψ * gaussSum (χ ^ n) ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
Tactic: rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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)) ψ
⊢ gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
have rw₁ : gaussSum (χ * χ ^ n) ψ * jacobiSum χ (χ ^ n) = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
Tactic: rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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)) ψ
⊢ gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
have rw₂ : jacobiSum χ (χ ^ n) * gaussSum (χ * χ ^ n) ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
Tactic: rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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)) ψ
⊢ gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
have rw₃ : jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
Tactic: rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
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 + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
have gauss_rw : 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']
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
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 + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
have ih₁ : gaussSum χ ψ ^ n * gaussSum χ ψ = (gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)) * gaussSum χ ψ
Tactic: apply_fun (· * gaussSum χ ψ) at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
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) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
have ih₁ : 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
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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)
⊢ gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
have succ : jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j) =
  gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
Tactic: rw [ih, Finset.prod_Ico_succ_top hn, mul_rotate, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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)
⊢ gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
have 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))
Tactic: rw [ih, Finset.prod_Ico_succ_top hn, mul_rotate, mul_assoc]