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
rw rw₁ rw₂ :
  Eq.{u_2 + 1} (α := R)
    (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((χ⁻¹ : (a : F) → R) (1 - x) : R) : R)
    (-(χ : (a : F) → R) (-1) : R)
rw₃ : Eq.{u_2 + 1} (α := R) (∑ x : F, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
⊢ jacobiSum χ χ⁻¹ = -(χ : (a : F) → R) (-1)
have rw₄ : Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
Tactic: classical
  rw [jacobiSum]
  conv => enter [1, 2, x]; rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]
  rw [sum_eq_sum_diff_singleton_add (mem_univ (1 : F)), sub_self, div_zero, χ.map_zero, add_zero]
  have : ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = ∑ x ∈ univ \ {-1}, χ x := by
    refine sum_bij' (fun a _ ↦ a / (1 - a)) (fun b _ ↦ b / (1 + b)) (fun x hx ↦ ?_)
      (fun y hy ↦ ?_) (fun x hx ↦ ?_) (fun y hy ↦ ?_) (fun _ _ ↦ rfl)
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx ⊢
      rw [div_eq_iff <| sub_ne_zero.mpr ((ne_eq ..).symm ▸ hx).symm, mul_sub, mul_one,
        neg_one_mul, sub_neg_eq_add, right_eq_add, neg_eq_zero]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy ⊢
      rw [div_eq_iff fun h ↦ hy <| eq_neg_of_add_eq_zero_right h, one_mul, right_eq_add]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx
      rw [eq_comm, ← sub_eq_zero] at hx
      simp [field]
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy
      rw [eq_comm, neg_eq_iff_eq_neg, ← sub_eq_zero, sub_neg_eq_add] at hy
      simp [field]
  rw [this, ← add_eq_zero_iff_eq_neg, ← sum_eq_sum_diff_singleton_add (mem_univ (-1 : F))]
  exact MulChar.sum_eq_zero_of_ne_one hχ
-- 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
rw rw₁ rw₂ :
  Eq.{u_2 + 1} (α := R)
    (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((χ⁻¹ : (a : F) → R) (1 - x) : R) : R)
    (-(χ : (a : F) → R) (-1) : R)
rw₃ : Eq.{u_2 + 1} (α := R) (∑ x : F, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
rw₄ : Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
⊢ jacobiSum χ χ⁻¹ = -(χ : (a : F) → R) (-1)
have rw₅ : ∀
  (this :
    Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x))) (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)),
  Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
Tactic: classical
  rw [jacobiSum]
  conv => enter [1, 2, x]; rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]
  rw [sum_eq_sum_diff_singleton_add (mem_univ (1 : F)), sub_self, div_zero, χ.map_zero, add_zero]
  have : ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = ∑ x ∈ univ \ {-1}, χ x := by
    refine sum_bij' (fun a _ ↦ a / (1 - a)) (fun b _ ↦ b / (1 + b)) (fun x hx ↦ ?_)
      (fun y hy ↦ ?_) (fun x hx ↦ ?_) (fun y hy ↦ ?_) (fun _ _ ↦ rfl)
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx ⊢
      rw [div_eq_iff <| sub_ne_zero.mpr ((ne_eq ..).symm ▸ hx).symm, mul_sub, mul_one,
        neg_one_mul, sub_neg_eq_add, right_eq_add, neg_eq_zero]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy ⊢
      rw [div_eq_iff fun h ↦ hy <| eq_neg_of_add_eq_zero_right h, one_mul, right_eq_add]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx
      rw [eq_comm, ← sub_eq_zero] at hx
      simp [field]
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy
      rw [eq_comm, neg_eq_iff_eq_neg, ← sub_eq_zero, sub_neg_eq_add] at hy
      simp [field]
  rw [this, ← add_eq_zero_iff_eq_neg, ← sum_eq_sum_diff_singleton_add (mem_univ (-1 : F))]
  exact MulChar.sum_eq_zero_of_ne_one hχ
-- 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
rw rw₁ rw₂ :
  Eq.{u_2 + 1} (α := R)
    (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((χ⁻¹ : (a : F) → R) (1 - x) : R) : R)
    (-(χ : (a : F) → R) (-1) : R)
rw₃ : Eq.{u_2 + 1} (α := R) (∑ x : F, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
rw₄ : Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
rw₅ :
  ∀
    (this :
      Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x)))
        (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)),
    Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
⊢ jacobiSum χ χ⁻¹ = -(χ : (a : F) → R) (-1)
have rw₆ : ∀
  (this :
    Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x))) (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)),
  Eq.{u_2 + 1} (α := R) (∑ x : F, (χ : (a : F) → R) x) 0
Tactic: classical
  rw [jacobiSum]
  conv => enter [1, 2, x]; rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]
  rw [sum_eq_sum_diff_singleton_add (mem_univ (1 : F)), sub_self, div_zero, χ.map_zero, add_zero]
  have : ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = ∑ x ∈ univ \ {-1}, χ x := by
    refine sum_bij' (fun a _ ↦ a / (1 - a)) (fun b _ ↦ b / (1 + b)) (fun x hx ↦ ?_)
      (fun y hy ↦ ?_) (fun x hx ↦ ?_) (fun y hy ↦ ?_) (fun _ _ ↦ rfl)
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx ⊢
      rw [div_eq_iff <| sub_ne_zero.mpr ((ne_eq ..).symm ▸ hx).symm, mul_sub, mul_one,
        neg_one_mul, sub_neg_eq_add, right_eq_add, neg_eq_zero]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy ⊢
      rw [div_eq_iff fun h ↦ hy <| eq_neg_of_add_eq_zero_right h, one_mul, right_eq_add]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx
      rw [eq_comm, ← sub_eq_zero] at hx
      simp [field]
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy
      rw [eq_comm, neg_eq_iff_eq_neg, ← sub_eq_zero, sub_neg_eq_add] at hy
      simp [field]
  rw [this, ← add_eq_zero_iff_eq_neg, ← sum_eq_sum_diff_singleton_add (mem_univ (-1 : F))]
  exact MulChar.sum_eq_zero_of_ne_one hχ
-- 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 χ φ =
  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: rw [gaussSum_mul _ _ ψ, sum_eq_sum_diff_singleton_add (mem_univ (0 : F))]
-- 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 χ φ =
    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))
have h₁ : ∀ (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: enter [2, 2, 2, x]
-- 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
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)
have h₁ : HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) (-1) : R) ((χ * φ : (a : F) → R) x : R)
Tactic: 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]
-- 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 χ φ =
    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))
have h₁ : ∀ (x : F), HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) (-1) : R) ((χ * φ : (a : F) → R) x : R)
Tactic: 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]
-- 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 χ φ =
    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))
have conv : 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: 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]
-- 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 χ φ =
    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))
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: rw [← mul_sum _ _ (φ (-1)), MulChar.sum_eq_zero_of_ne_one h, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
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
t : F
ht : 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)
have ht₁ : ¬t = 0
Tactic: simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
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 χ φ =
    ∑ 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)
have 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)
Tactic: 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
-- 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)
⊢ 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)
have simp_rw : gaussSum (χ * φ) ψ * jacobiSum χ φ =
  ∑ x ∈ univ \ {0},
    HMul.hMul (α := R) (β := R)
      (∑ x_1 : F,
          HMul.hMul (α := R) ((χ : (a : F) → R) x : R)
            (HMul.hMul (α := R) ((χ : (a : F) → R) x_1 : R)
              (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) x : R) ((φ : (a : F) → R) (1 - x_1) : R))) :
        R)
      ((ψ : (a : F) → R) x : R)
Tactic: simp_rw [← sum_mul, sum_congr rfl sum_eq, ← mul_one_sub, map_mul, mul_assoc]
-- 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)
| gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R)
        (∑ x_1 : F,
            HMul.hMul (α := R) ((χ : (a : F) → R) x : R)
              (HMul.hMul (α := R) ((χ : (a : F) → R) x_1 : R)
                (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) x : R) ((φ : (a : F) → R) (1 - x_1) : R))) :
          R)
        ((ψ : (a : F) → R) x : R)
have h₁ : ∀ (t x : F),
  HMul.hMul (α := R) ((χ : (a : F) → R) x : R)
    (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) t : R) ((φ : (a : F) → R) (1 - x) : R))
Tactic: enter [2, 2, t, 1, 2, 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 : 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)
t x : F
| HMul.hMul (α := R) ((χ : (a : F) → R) x : R)
    (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) t : R) ((φ : (a : F) → R) (1 - x) : R))
have h₁ : HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) t : R) ((χ : (a : F) → R) x : R))
  ((φ : (a : F) → R) (1 - x) : R)
Tactic: rw [← mul_assoc, mul_comm (χ x) (φ t)]
-- 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)
| gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R)
        (∑ x_1 : F,
            HMul.hMul (α := R) ((χ : (a : F) → R) x : R)
              (HMul.hMul (α := R) ((χ : (a : F) → R) x_1 : R)
                (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) x : R) ((φ : (a : F) → R) (1 - x_1) : R))) :
          R)
        ((ψ : (a : F) → R) x : R)
have h₁ : ∀ (t x : F),
  HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) t : R) ((χ : (a : F) → R) x : R))
    ((φ : (a : F) → R) (1 - x) : R)
Tactic: enter [2, 2, t, 1, 2, x, 2]; rw [← mul_assoc, mul_comm (χ x) (φ t)]
-- 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)
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R)
        (∑ x_1 : F,
            HMul.hMul (α := R) ((χ : (a : F) → R) x : R)
              (HMul.hMul (α := R) ((χ : (a : F) → R) x_1 : R)
                (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) x : R) ((φ : (a : F) → R) (1 - x_1) : R))) :
          R)
        ((ψ : (a : F) → R) x : R)
have conv : gaussSum (χ * φ) ψ * jacobiSum χ φ =
  ∑ t ∈ univ \ {0},
    HMul.hMul (α := R) (β := R)
      (∑ x : F,
          HMul.hMul (α := R) ((χ : (a : F) → R) t : R)
            (HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) t : R) ((χ : (a : F) → R) x : R))
              ((φ : (a : F) → R) (1 - x) : R)) :
        R)
      ((ψ : (a : F) → R) t : R)
Tactic: conv => enter [2, 2, t, 1, 2, x, 2]; rw [← mul_assoc, mul_comm (χ x) (φ t)]
-- 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)
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ t ∈ univ \ {0},
      HMul.hMul (α := R) (β := R)
        (∑ x : F,
            HMul.hMul (α := R) ((χ : (a : F) → R) t : R)
              (HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) t : R) ((χ : (a : F) → R) x : R))
                ((φ : (a : F) → R) (1 - x) : R)) :
          R)
        ((ψ : (a : F) → R) t : R)
have simp_rw : 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)
Tactic: simp_rw [← mul_assoc, ← MulChar.mul_apply, mul_assoc, ← mul_sum, mul_right_comm]
-- 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)
⊢ 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 : gaussSum (χ * φ) ψ * jacobiSum χ φ =
  ∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : 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 χ φ
⊢ 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₁ : gaussSum (χ * φ) ψ * 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]