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 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq :
  ∀ (t : F),
    Membership.mem (γ := Finset F) (univ \ {0}) t →
      HMul.hMul (α := R) (β := R)
          (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R) : R)
          ((ψ : (a : F) → R) t : R) =
        HMul.hMul (α := R) (β := R)
          (∑ y : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (t * y) : R) ((φ : (a : F) → R) (t - t * y) : R) : R)
          ((ψ : (a : F) → R) t : R)
rw :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) * jacobiSum χ φ
rw₁ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) *
        ∑ i : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) i : R) ((φ : (a : F) → R) (1 - i) : R)
have rw₂ : (∑ a : F, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) a : R) ((ψ : (a : F) → R) a : R)) * jacobiSum χ φ =
  (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
    jacobiSum χ φ
Tactic: rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, 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 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq :
  ∀ (t : F),
    Membership.mem (γ := Finset F) (univ \ {0}) t →
      HMul.hMul (α := R) (β := R)
          (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R) : R)
          ((ψ : (a : F) → R) t : R) =
        HMul.hMul (α := R) (β := R)
          (∑ y : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (t * y) : R) ((φ : (a : F) → R) (t - t * y) : R) : R)
          ((ψ : (a : F) → R) t : R)
rw :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) * jacobiSum χ φ
rw₁ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₂ :
  (∑ a : F, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) a : R) ((ψ : (a : F) → R) a : R)) * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) *
        ∑ i : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) i : R) ((φ : (a : F) → R) (1 - i) : R)
have rw₃ : (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) +
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) 0 : R) ((ψ : (a : F) → R) 0 : R)) *
    jacobiSum χ φ =
  (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
    jacobiSum χ φ
Tactic: rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, 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 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq :
  ∀ (t : F),
    Membership.mem (γ := Finset F) (univ \ {0}) t →
      HMul.hMul (α := R) (β := R)
          (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R) : R)
          ((ψ : (a : F) → R) t : R) =
        HMul.hMul (α := R) (β := R)
          (∑ y : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (t * y) : R) ((φ : (a : F) → R) (t - t * y) : R) : R)
          ((ψ : (a : F) → R) t : R)
rw :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) * jacobiSum χ φ
rw₁ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₂ :
  (∑ a : F, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) a : R) ((ψ : (a : F) → R) a : R)) * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₃ :
  (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) +
        HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) 0 : R) ((ψ : (a : F) → R) 0 : R)) *
      jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) *
        ∑ i : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) i : R) ((φ : (a : F) → R) (1 - i) : R)
have rw₄ : (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) +
      HMul.hMul (α := R) (β := R) (0 : R) ((ψ : (a : F) → R) 0 : R)) *
    jacobiSum χ φ =
  (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
    jacobiSum χ φ
Tactic: rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, 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 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq :
  ∀ (t : F),
    Membership.mem (γ := Finset F) (univ \ {0}) t →
      HMul.hMul (α := R) (β := R)
          (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R) : R)
          ((ψ : (a : F) → R) t : R) =
        HMul.hMul (α := R) (β := R)
          (∑ y : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (t * y) : R) ((φ : (a : F) → R) (t - t * y) : R) : R)
          ((ψ : (a : F) → R) t : R)
rw :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) * jacobiSum χ φ
rw₁ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₂ :
  (∑ a : F, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) a : R) ((ψ : (a : F) → R) a : R)) * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₃ :
  (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) +
        HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) 0 : R) ((ψ : (a : F) → R) 0 : R)) *
      jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₄ :
  (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) +
        HMul.hMul (α := R) (β := R) (0 : R) ((ψ : (a : F) → R) 0 : R)) *
      jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) *
        ∑ i : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) i : R) ((φ : (a : F) → R) (1 - i) : R)
have rw₅ : HAdd.hAdd (α := R)
      (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R)) 0 *
    jacobiSum χ φ =
  (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
    jacobiSum χ φ
Tactic: rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, 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 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq :
  ∀ (t : F),
    Membership.mem (γ := Finset F) (univ \ {0}) t →
      HMul.hMul (α := R) (β := R)
          (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R) : R)
          ((ψ : (a : F) → R) t : R) =
        HMul.hMul (α := R) (β := R)
          (∑ y : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (t * y) : R) ((φ : (a : F) → R) (t - t * y) : R) : R)
          ((ψ : (a : F) → R) t : R)
rw :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) * jacobiSum χ φ
rw₁ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₂ :
  (∑ a : F, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) a : R) ((ψ : (a : F) → R) a : R)) * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₃ :
  (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) +
        HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) 0 : R) ((ψ : (a : F) → R) 0 : R)) *
      jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₄ :
  (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) +
        HMul.hMul (α := R) (β := R) (0 : R) ((ψ : (a : F) → R) 0 : R)) *
      jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₅ :
  HAdd.hAdd (α := R)
        (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R)) 0 *
      jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) *
        ∑ i : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) i : R) ((φ : (a : F) → R) (1 - i) : R)
have rw₆ : (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R)) *
    jacobiSum χ φ =
  (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
    jacobiSum χ φ
Tactic: rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, 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 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ
have rw : gaussSum (χ * φ) ψ * jacobiSum χ φ =
  ∑ t : F,
    ∑ x : F,
      HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R))
        ((ψ : (a : F) → R) t : R)
Tactic: classical
  rw [gaussSum_mul _ _ ψ, sum_eq_sum_diff_singleton_add (mem_univ (0 : F))]
  conv =>
    enter [2, 2, 2, x]
    rw [zero_sub, neg_eq_neg_one_mul x, map_mul, mul_left_comm (χ x) (φ (-1)),
      ← MulChar.mul_apply, ψ.map_zero_eq_one, mul_one]
  rw [← mul_sum _ _ (φ (-1)), MulChar.sum_eq_zero_of_ne_one h, mul_zero, add_zero]
  have sum_eq : ∀ t ∈ univ \ {0}, (∑ x : F, χ x * φ (t - x)) * ψ t =
      (∑ y : F, χ (t * y) * φ (t - (t * y))) * ψ t := by
    intro t ht
    simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at ht
    exact congrArg (· * ψ t) (Equiv.sum_comp (Equiv.mulLeft₀ t ht) _).symm
  simp_rw [← sum_mul, sum_congr rfl sum_eq, ← mul_one_sub, map_mul, mul_assoc]
  conv => enter [2, 2, t, 1, 2, x, 2]; rw [← mul_assoc, mul_comm (χ x) (φ t)]
  simp_rw [← mul_assoc, ← MulChar.mul_apply, mul_assoc, ← mul_sum, mul_right_comm]
  rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, 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 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
rw :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ t : F,
      ∑ x : F,
        HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R))
          ((ψ : (a : F) → R) t : R)
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ
have rw₁ : gaussSum (χ * φ) ψ * jacobiSum χ φ =
  HAdd.hAdd (α := R)
    (∑ x ∈ univ \ {0},
      ∑ x_1 : F,
        HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x_1 : R) ((φ : (a : F) → R) (x - x_1) : R))
          ((ψ : (a : F) → R) x : R))
    (∑ x : F,
      HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (0 - x) : R))
        ((ψ : (a : F) → R) 0 : R))
Tactic: classical
  rw [gaussSum_mul _ _ ψ, sum_eq_sum_diff_singleton_add (mem_univ (0 : F))]
  conv =>
    enter [2, 2, 2, x]
    rw [zero_sub, neg_eq_neg_one_mul x, map_mul, mul_left_comm (χ x) (φ (-1)),
      ← MulChar.mul_apply, ψ.map_zero_eq_one, mul_one]
  rw [← mul_sum _ _ (φ (-1)), MulChar.sum_eq_zero_of_ne_one h, mul_zero, add_zero]
  have sum_eq : ∀ t ∈ univ \ {0}, (∑ x : F, χ x * φ (t - x)) * ψ t =
      (∑ y : F, χ (t * y) * φ (t - (t * y))) * ψ t := by
    intro t ht
    simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at ht
    exact congrArg (· * ψ t) (Equiv.sum_comp (Equiv.mulLeft₀ t ht) _).symm
  simp_rw [← sum_mul, sum_congr rfl sum_eq, ← mul_one_sub, map_mul, mul_assoc]
  conv => enter [2, 2, t, 1, 2, x, 2]; rw [← mul_assoc, mul_comm (χ x) (φ t)]
  simp_rw [← mul_assoc, ← MulChar.mul_apply, mul_assoc, ← mul_sum, mul_right_comm]
  rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, 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 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
rw :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ t : F,
      ∑ x : F,
        HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R))
          ((ψ : (a : F) → R) t : R)
rw₁ rw₂ rw₃ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    HAdd.hAdd (α := R)
      (∑ x ∈ univ \ {0},
        ∑ x_1 : F,
          HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x_1 : R) ((φ : (a : F) → R) (x - x_1) : R))
            ((ψ : (a : F) → R) x : R))
      (∑ x : F,
        HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (0 - x) : R))
          ((ψ : (a : F) → R) 0 : R))
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ
have rw₄ : gaussSum (χ * φ) ψ * jacobiSum χ φ =
  HAdd.hAdd (α := R)
    (∑ x ∈ univ \ {0},
      ∑ x_1 : F,
        HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x_1 : R) ((φ : (a : F) → R) (x - x_1) : R))
          ((ψ : (a : F) → R) x : R))
    (∑ x : F, HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) (-1) : R) ((χ * φ : (a : F) → R) x : R))
Tactic: classical
  rw [gaussSum_mul _ _ ψ, sum_eq_sum_diff_singleton_add (mem_univ (0 : F))]
  conv =>
    enter [2, 2, 2, x]
    rw [zero_sub, neg_eq_neg_one_mul x, map_mul, mul_left_comm (χ x) (φ (-1)),
      ← MulChar.mul_apply, ψ.map_zero_eq_one, mul_one]
  rw [← mul_sum _ _ (φ (-1)), MulChar.sum_eq_zero_of_ne_one h, mul_zero, add_zero]
  have sum_eq : ∀ t ∈ univ \ {0}, (∑ x : F, χ x * φ (t - x)) * ψ t =
      (∑ y : F, χ (t * y) * φ (t - (t * y))) * ψ t := by
    intro t ht
    simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at ht
    exact congrArg (· * ψ t) (Equiv.sum_comp (Equiv.mulLeft₀ t ht) _).symm
  simp_rw [← sum_mul, sum_congr rfl sum_eq, ← mul_one_sub, map_mul, mul_assoc]
  conv => enter [2, 2, t, 1, 2, x, 2]; rw [← mul_assoc, mul_comm (χ x) (φ t)]
  simp_rw [← mul_assoc, ← MulChar.mul_apply, mul_assoc, ← mul_sum, mul_right_comm]
  rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, 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 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
rw :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ t : F,
      ∑ x : F,
        HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R))
          ((ψ : (a : F) → R) t : R)
rw₁ rw₂ rw₃ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    HAdd.hAdd (α := R)
      (∑ x ∈ univ \ {0},
        ∑ x_1 : F,
          HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x_1 : R) ((φ : (a : F) → R) (x - x_1) : R))
            ((ψ : (a : F) → R) x : R))
      (∑ x : F,
        HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (0 - x) : R))
          ((ψ : (a : F) → R) 0 : R))
rw₄ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    HAdd.hAdd (α := R)
      (∑ x ∈ univ \ {0},
        ∑ x_1 : F,
          HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x_1 : R) ((φ : (a : F) → R) (x - x_1) : R))
            ((ψ : (a : F) → R) x : R))
      (∑ x : F, HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) (-1) : R) ((χ * φ : (a : F) → R) x : R))
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ
have rw₅ : gaussSum (χ * φ) ψ * jacobiSum χ φ =
  ∑ x ∈ univ \ {0},
    ∑ x_1 : F,
      HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x_1 : R) ((φ : (a : F) → R) (x - x_1) : R))
        ((ψ : (a : F) → R) x : R)
Tactic: classical
  rw [gaussSum_mul _ _ ψ, sum_eq_sum_diff_singleton_add (mem_univ (0 : F))]
  conv =>
    enter [2, 2, 2, x]
    rw [zero_sub, neg_eq_neg_one_mul x, map_mul, mul_left_comm (χ x) (φ (-1)),
      ← MulChar.mul_apply, ψ.map_zero_eq_one, mul_one]
  rw [← mul_sum _ _ (φ (-1)), MulChar.sum_eq_zero_of_ne_one h, mul_zero, add_zero]
  have sum_eq : ∀ t ∈ univ \ {0}, (∑ x : F, χ x * φ (t - x)) * ψ t =
      (∑ y : F, χ (t * y) * φ (t - (t * y))) * ψ t := by
    intro t ht
    simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at ht
    exact congrArg (· * ψ t) (Equiv.sum_comp (Equiv.mulLeft₀ t ht) _).symm
  simp_rw [← sum_mul, sum_congr rfl sum_eq, ← mul_one_sub, map_mul, mul_assoc]
  conv => enter [2, 2, t, 1, 2, x, 2]; rw [← mul_assoc, mul_comm (χ x) (φ t)]
  simp_rw [← mul_assoc, ← MulChar.mul_apply, mul_assoc, ← mul_sum, mul_right_comm]
  rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : Ne.{u_2 + 1} (α := F') (↑(Fintype.card F) : F') 0
χ φ : MulChar F F'
hχφ : χ * φ ≠ 1
ψ : AddChar F F'
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := F') ψ
⊢ jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ / gaussSum (χ * φ) ψ
have rw : gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ
Tactic: rw [eq_div_iff <| gaussSum_ne_zero_of_nontrivial h hχφ hψ, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
⊢ jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = (↑(Fintype.card F) : F')
have obtain : ∀ (n : ℕ+) (hp : Nat.Prime (ringChar F)) (hc : Fintype.card F = ringChar F ^ (↑n : ℕ)),
  jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = (↑(Fintype.card F) : F')
Tactic: obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
⊢ jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = (↑(Fintype.card F) : F')
have hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Tactic: have hinj := (algebraMap F' FF').injective
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
⊢ jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = (↑(Fintype.card F) : F')
have a : Eq (α := FF') (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹) : FF')
  (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F') : FF')
Tactic: apply hinj
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
⊢ Eq (α := FF') (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹) : FF')
    (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F') : FF')
have a : jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
    jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF')) =
  ((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F')
Tactic: rw [map_mul, ← jacobiSum_ringHomComp, ← jacobiSum_ringHomComp]