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 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx : ¬x = 1
⊢ ¬Eq.{u_1 + 1} (α := F) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
x : F
hx : ¬x = 1
⊢ ¬Eq.{u_1 + 1} (α := F) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
y : F
hy : Membership.mem (γ := Finset F) (univ \ {-1}) y
refine_2 : ∀ (hy : ¬y = -1), ¬y / (1 + y) = 1
⊢ Membership.mem (γ := Finset F) (univ \ {1})
    ((fun (b : F) (x : Membership.mem (γ := Finset F) (univ \ {-1}) b) ↦ b / (1 + b)) y hy)

Tactic:
simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy ⊢

Premises used: Finset.mem_univ, Finset.mem_singleton, Finset.mem_sdiff, true_and
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
y : F
hy : ¬y = -1
refine_2 : ¬Eq.{u_1 + 1} (α := F) 1 0
⊢ ¬y / (1 + y) = 1

Tactic:
rw [div_eq_iff fun h ↦ hy <| eq_neg_of_add_eq_zero_right h, one_mul, right_eq_add]

Premises used: div_eq_iff, eq_neg_of_add_eq_zero_right, right_eq_add, one_mul
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
y : F
hy : ¬y = -1
⊢ ¬Eq.{u_1 + 1} (α := F) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
y : F
hy : ¬y = -1
⊢ ¬Eq.{u_1 + 1} (α := F) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
x : F
hx : Membership.mem (γ := Finset F) (univ \ {1}) x
⊢ ¬x = 1

Tactic:
simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx

Premises used: Finset.mem_univ, Finset.mem_singleton, Finset.mem_sdiff, true_and
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
x : F
hx_1 : Membership.mem (γ := Finset F) (univ \ {1}) x
hx : ¬x = 1
⊢ ¬1 - x = 0

Tactic:
rw [eq_comm, ← sub_eq_zero] at hx

Premises used: sub_eq_zero, eq_comm
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
x : F
hx_1 : Membership.mem (γ := Finset F) (univ \ {1}) x
hx : ¬1 - x = 0
⊢ (fun (b : F) (x : Membership.mem (γ := Finset F) (univ \ {-1}) b) ↦ b / (1 + b))
      ((fun (a : F) (x : Membership.mem (γ := Finset F) (univ \ {1}) a) ↦ a / (1 - a)) x hx_1) ⋯ =
    x

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
y : F
hy : Membership.mem (γ := Finset F) (univ \ {-1}) y
⊢ ¬y = -1

Tactic:
simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy

Premises used: Finset.mem_univ, Finset.mem_singleton, Finset.mem_sdiff, true_and
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
y : F
hy_1 : Membership.mem (γ := Finset F) (univ \ {-1}) y
hy : ¬y = -1
⊢ ¬1 + y = 0

Tactic:
rw [eq_comm, neg_eq_iff_eq_neg, ← sub_eq_zero, sub_neg_eq_add] at hy

Premises used: sub_eq_zero, neg_eq_iff_eq_neg, eq_comm, sub_neg_eq_add
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
y : F
hy_1 : Membership.mem (γ := Finset F) (univ \ {-1}) y
hy : ¬1 + y = 0
⊢ (fun (a : F) (x : Membership.mem (γ := Finset F) (univ \ {1}) a) ↦ a / (1 - a))
      ((fun (b : F) (x : Membership.mem (γ := Finset F) (univ \ {-1}) b) ↦ b / (1 + b)) y hy_1) ⋯ =
    y

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x))) (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)

Tactic:
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]
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
this :
  Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x))) (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)
rw : Eq.{u_2 + 1} (α := R) (∑ x : F, (χ : (a : F) → R) x) 0
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)

Tactic:
rw [this, ← add_eq_zero_iff_eq_neg, ← sum_eq_sum_diff_singleton_add (mem_univ (-1 : F))]

Premises used: Finset.mem_univ, Finset.sum_eq_sum_diff_singleton_add, add_eq_zero_iff_eq_neg, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
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:
MulChar.sum_eq_zero_of_ne_one hχ

Premises used: MulChar.sum_eq_zero_of_ne_one
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
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:
exact MulChar.sum_eq_zero_of_ne_one hχ

Premises used: MulChar.sum_eq_zero_of_ne_one
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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)
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
⊢ jacobiSum χ χ⁻¹ = -(χ : (a : F) → R) (-1)

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χ

Premises used: sub_self, add_eq_zero_iff_eq_neg, jacobiSum, div_eq_mul_inv, map_mul, MulChar.inv_apply', add_zero, MulChar.map_zero, div_zero, MulChar.sum_eq_zero_of_ne_one
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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 χ φ =
    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 φ ψ

Tactic:
rw [gaussSum_mul _ _ ψ, sum_eq_sum_diff_singleton_add (mem_univ (0 : F))]

Premises used: Finset.mem_univ, gaussSum_mul, Finset.sum_eq_sum_diff_singleton_add, OfNat.ofNat
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
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)
| 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:
enter [2, 2, 2, x]
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
h₁ : HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) (-1) : R) ((χ * φ : (a : F) → R) x : R)
| 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 [zero_sub, neg_eq_neg_one_mul x, map_mul, mul_left_comm (χ x) (φ (-1)),
      ← MulChar.mul_apply, ψ.map_zero_eq_one, mul_one]

Premises used: AddChar.map_zero_eq_one, mul_left_comm, MulChar.mul_apply, map_mul, neg_eq_neg_one_mul, mul_one, OfNat.ofNat, DFunLike.coe, Neg.neg, zero_sub
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
h₁ : ∀ (x : F), HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) (-1) : R) ((χ * φ : (a : F) → R) x : 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))

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]

Premises used: AddChar.map_zero_eq_one, MulChar.mul_apply, map_mul, mul_one, zero_sub
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
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))
⊢ 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:
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]

Premises used: AddChar.map_zero_eq_one, MulChar.mul_apply, map_mul, mul_one, zero_sub
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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 χ φ =
    ∑ 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)
⊢ 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:
rw [← mul_sum _ _ (φ (-1)), MulChar.sum_eq_zero_of_ne_one h, mul_zero, add_zero]

Premises used: Finset.mul_sum, MulZeroClass.mul_zero, add_zero, OfNat.ofNat, DFunLike.coe, MulChar.sum_eq_zero_of_ne_one, Neg.neg
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
⊢ ¬t = 0

Tactic:
simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at ht

Premises used: Finset.mem_univ, Finset.mem_singleton, Finset.mem_sdiff, true_and
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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 : ¬t = 0
⊢ 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:
congrArg (· * ψ t) (Equiv.sum_comp (Equiv.mulLeft₀ t ht) _).symm

Premises used: HMul.hMul, congrArg, Equiv.sum_comp, Equiv.mulLeft₀, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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 : ¬t = 0
⊢ 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:
exact congrArg (· * ψ t) (Equiv.sum_comp (Equiv.mulLeft₀ t ht) _).symm

Premises used: HMul.hMul, congrArg, Equiv.sum_comp, Equiv.mulLeft₀, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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),
    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
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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)
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)
⊢ 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:
simp_rw [← sum_mul, sum_congr rfl sum_eq, ← mul_one_sub, map_mul, mul_assoc]

Premises used: mul_assoc, mul_one_sub, map_mul, Finset.sum_congr, rfl, Finset.sum_mul
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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)
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))
| 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:
enter [2, 2, t, 1, 2, x, 2]
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
h₁ :
  HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) t : R) ((χ : (a : F) → R) x : R))
    ((φ : (a : F) → R) (1 - x) : R)
| HMul.hMul (α := R) ((χ : (a : F) → R) x : R)
    (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) t : R) ((φ : (a : F) → R) (1 - x) : R))

Tactic:
rw [← mul_assoc, mul_comm (χ x) (φ t)]

Premises used: mul_assoc, mul_comm, DFunLike.coe
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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)
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)
| 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:
enter [2, 2, t, 1, 2, x, 2]; rw [← mul_assoc, mul_comm (χ x) (φ t)]

Premises used: mul_assoc