awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
simp :
  Eq.{v + 1} (α := R')
    (∑ i : R,
      HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R')
        (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') ((↑a : R) * i) : R')))
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((ψ : (a : R) → R') a : R'))
⊢ HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R') (gaussSum χ (ψ.mulShift (↑a : R))) = gaussSum χ ψ

Tactic:
simp only [gaussSum, mulShift_apply, Finset.mul_sum]

Premises used: Finset.mul_sum, AddChar.mulShift_apply, gaussSum
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
simp_rw :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') ((↑a : R) * x) : R') ((ψ : (a : R) → R') ((↑a : R) * x) : R'))
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((ψ : (a : R) → R') a : R'))
⊢ Eq.{v + 1} (α := R')
    (∑ i : R,
      HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R')
        (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') ((↑a : R) * i) : R')))
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((ψ : (a : R) → R') a : R'))

Tactic:
simp_rw [← mul_assoc, ← map_mul]

Premises used: mul_assoc, map_mul
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') ((↑a : R) * x) : R') ((ψ : (a : R) → R') ((↑a : R) * x) : R'))
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((ψ : (a : R) → R') a : R'))

Tactic:
Fintype.sum_bijective _ a.mulLeft_bijective _ _ fun x ↦ rfl

Premises used: Fintype.sum_bijective, Units.mulLeft_bijective, rfl
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') ((↑a : R) * x) : R') ((ψ : (a : R) → R') ((↑a : R) * x) : R'))
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((ψ : (a : R) → R') a : R'))

Tactic:
exact Fintype.sum_bijective _ a.mulLeft_bijective _ _ fun x ↦ rfl

Premises used: Fintype.sum_bijective, Units.mulLeft_bijective, rfl
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
rw :
  gaussSum χ (ψ.mulShift (↑a : R)) =
    HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (↑a : R) : R')
      (HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R') (gaussSum χ (ψ.mulShift (↑a : R))))
rw₁ :
  gaussSum χ (ψ.mulShift (↑a : R)) =
    HMul.hMul (α := R') (Ring.inverse ((χ : (a : R) → R') (↑a : R)) : R')
      (HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R') (gaussSum χ (ψ.mulShift (↑a : R))))
rw₂ rw₃ : gaussSum χ (ψ.mulShift (↑a : R)) = gaussSum χ (ψ.mulShift (↑a : R))
⊢ gaussSum χ (ψ.mulShift (↑a : R)) = HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (↑a : R) : R') (gaussSum χ ψ)

Tactic:
rw [← gaussSum_mulShift χ ψ a, inv_apply_eq_inv,
    Ring.inverse_mul_cancel_left _ _ (a.isUnit.map χ)]

Premises used: MulChar.inv_apply_eq_inv, Ring.inverse_mul_cancel_left, IsUnit.map, Units.isUnit, gaussSum_mulShift
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
χ : MulChar R ℂ
ψ : AddChar R ℂ
⊢ star (gaussSum χ ψ) =
    ∑ x : R, HMul.hMul (α := ℂ) (β := ℂ) (star ((ψ : (a : R) → ℂ) x) : ℂ) ((χ⁻¹ : (a : R) → ℂ) x : ℂ)

Tactic:
simp [gaussSum, star_mul, MulChar.star_apply']

Premises used: MulChar.star_apply', gaussSum, StarMul.star_mul
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
χ : MulChar R ℂ
ψ : AddChar R ℂ
⊢ Eq (α := ℂ) (∑ x : R, HMul.hMul (α := ℂ) (β := ℂ) (star ((ψ : (a : R) → ℂ) x) : ℂ) ((χ⁻¹ : (a : R) → ℂ) x : ℂ))
    (∑ x : R, HMul.hMul (α := ℂ) (β := ℂ) ((ψ⁻¹ : (a : R) → ℂ) x : ℂ) ((χ⁻¹ : (a : R) → ℂ) x : ℂ))

Tactic:
simp [← starRingEnd_apply, map_neg_eq_conj]

Premises used: starRingEnd_apply, AddChar.map_neg_eq_conj
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
χ : MulChar R ℂ
ψ : AddChar R ℂ
⊢ ∑ x : R, HMul.hMul (α := ℂ) (β := ℂ) ((ψ⁻¹ : (a : R) → ℂ) x : ℂ) ((χ⁻¹ : (a : R) → ℂ) x : ℂ) = gaussSum χ⁻¹ ψ⁻¹

Tactic:
simp [mul_comm, gaussSum]

Premises used: gaussSum, mul_comm
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
rw :
  Eq.{v + 1} (α := R')
    (∑ i : R,
      ∑ j : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
          HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') j : R') ((ψ : (a : R) → R') j : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
⊢ gaussSum χ ψ * gaussSum φ ψ =
    ∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R')

Tactic:
rw [gaussSum, gaussSum, sum_mul_sum]

Premises used: gaussSum, Finset.sum_mul_sum
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
h :
  ∀ (x x_1 : R),
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') x : R') *
      HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') x_1 : R') ((ψ : (a : R) → R') x_1 : R')
| Eq.{v + 1} (α := R')
    (∑ i : R,
      ∑ j : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
          HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') j : R') ((ψ : (a : R) → R') j : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))

Tactic:
enter [1, 2, x, 2, x_1]
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x x_1 : R
h :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R') *
    HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') x : R') ((ψ : (a : R) → R') x_1 : R')
| HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') x : R') *
    HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') x_1 : R') ((ψ : (a : R) → R') x_1 : R')

Tactic:
rw [mul_mul_mul_comm]

Premises used: mul_mul_mul_comm
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
h :
  ∀ (x x_1 : R),
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R') *
      HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') x : R') ((ψ : (a : R) → R') x_1 : R')
| Eq.{v + 1} (α := R')
    (∑ i : R,
      ∑ j : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
          HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') j : R') ((ψ : (a : R) → R') j : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))

Tactic:
enter [1, 2, x, 2, x_1]; rw [mul_mul_mul_comm]

Premises used: mul_mul_mul_comm
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
conv :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ x_1 : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R') *
          HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') x : R') ((ψ : (a : R) → R') x_1 : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
⊢ Eq.{v + 1} (α := R')
    (∑ i : R,
      ∑ j : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
          HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') j : R') ((ψ : (a : R) → R') j : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))

Tactic:
conv => enter [1, 2, x, 2, x_1]; rw [mul_mul_mul_comm]

Premises used: mul_mul_mul_comm
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
simp :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ x_1 : R,
        HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R'))
          ((ψ : (a : R) → R') (x + x_1) : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ x_1 : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R') *
          HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') x : R') ((ψ : (a : R) → R') x_1 : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))

Tactic:
simp only [← ψ.map_add_eq_mul]

Premises used: AddChar.map_add_eq_mul
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
hi : ∀ (a : R) (ha : Membership.mem (γ := Finset R) univ a), Membership.mem (γ := Finset R) univ (a + x)
i_inj :
  ∀ (a₁ : R) (ha₁ : Membership.mem (γ := Finset R) univ a₁) (a₂ : R) (ha₂ : Membership.mem (γ := Finset R) univ a₂),
    a₁ + x = a₂ + x → a₁ = a₂
i_surj :
  ∀ (b : R), Membership.mem (γ := Finset R) univ b → ∃ (a : R) (_ : Membership.mem (γ := Finset R) univ a), a + x = b
h :
  ∀ (a : R) (ha : Membership.mem (γ := Finset R) univ a),
    HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
        ((ψ : (a : R) → R') (x + a) : R') =
      HMul.hMul (β := R')
        (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (a + x - x) : R'))
        ((ψ : (a : R) → R') (a + x) : R')
⊢ Eq.{v + 1} (α := R')
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') y : R'))
        ((ψ : (a : R) → R') (x + y) : R'))
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
        ((ψ : (a : R) → R') y : R'))

Tactic:
rw [sum_bij (fun a _ ↦ a + x)]

Premises used: Finset.sum_bij, HAdd.hAdd
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ (a : R) (ha : Membership.mem (γ := Finset R) univ a), Membership.mem (γ := Finset R) univ (a + x)

Tactic:
simp only [mem_univ, forall_const]

Premises used: Finset.mem_univ, forall_const
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ (a₁ : R) (ha₁ : Membership.mem (γ := Finset R) univ a₁) (a₂ : R) (ha₂ : Membership.mem (γ := Finset R) univ a₂),
    a₁ + x = a₂ + x → a₁ = a₂

Tactic:
simp only [mem_univ, add_left_inj, imp_self, forall_const]

Premises used: Finset.mem_univ, add_left_inj, imp_self, forall_const
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x b : R
h : Membership.mem (γ := Finset R) univ b
rw rw₁ : b = b
⊢ b - x + x = b

Tactic:
rw [sub_add_cancel]

Premises used: sub_add_cancel
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ (b : R), Membership.mem (γ := Finset R) univ b → ∃ (a : R) (_ : Membership.mem (γ := Finset R) univ a), a + x = b

Tactic:
exact fun b _ ↦ ⟨b - x, mem_univ _, by rw [sub_add_cancel]⟩
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x a : R
h : Membership.mem (γ := Finset R) univ a
rw :
  HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
      ((ψ : (a : R) → R') (x + a) : R') =
    HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
      ((ψ : (a : R) → R') (a + x) : R')
rw₁ rw₂ :
  HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
      ((ψ : (a : R) → R') (a + x) : R') =
    HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
      ((ψ : (a : R) → R') (a + x) : R')
⊢ HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
      ((ψ : (a : R) → R') (x + a) : R') =
    HMul.hMul (β := R')
      (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (a + x - x) : R'))
      ((ψ : (a : R) → R') (a + x) : R')

Tactic:
rw [add_sub_cancel_right, add_comm]

Premises used: add_comm, add_sub_cancel_right
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ (a : R) (ha : Membership.mem (γ := Finset R) univ a),
    HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
        ((ψ : (a : R) → R') (x + a) : R') =
      HMul.hMul (β := R')
        (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (a + x - x) : R'))
        ((ψ : (a : R) → R') (a + x) : R')

Tactic:
exact fun a _ ↦ by rw [add_sub_cancel_right, add_comm]
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ ∀ (x : R),
    Eq.{v + 1} (α := R')
      (∑ y : R,
        HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') y : R'))
          ((ψ : (a : R) → R') (x + y) : R'))
      (∑ y : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
          ((ψ : (a : R) → R') y : R'))

Tactic:
have sum_eq x : ∑ y : R, χ x * φ y * ψ (x + y) = ∑ y : R, χ x * φ (y - x) * ψ y := by
    rw [sum_bij (fun a _ ↦ a + x)]
    · simp only [mem_univ, forall_const]
    · simp only [mem_univ, add_left_inj, imp_self, forall_const]
    · exact fun b _ ↦ ⟨b - x, mem_univ _, by rw [sub_add_cancel]⟩
    · exact fun a _ ↦ by rw [add_sub_cancel_right, add_comm]
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
sum_eq :
  ∀ (x : R),
    Eq.{v + 1} (α := R')
      (∑ y : R,
        HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') y : R'))
          ((ψ : (a : R) → R') (x + y) : R'))
      (∑ y : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
          ((ψ : (a : R) → R') y : R'))
rw :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ y : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
          ((ψ : (a : R) → R') y : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
rw₁ rw₂ :
  Eq.{v + 1} (α := R')
    (∑ y : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
          ((ψ : (a : R) → R') y : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ x_1 : R,
        HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R'))
          ((ψ : (a : R) → R') (x + x_1) : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))

Tactic:
rw [sum_congr rfl fun x _ ↦ sum_eq x, sum_comm]

Premises used: Finset.sum_comm, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
rw : HMul.hMul (α := R') ((χ : (a : R) → R') (↑(-1) : R) : R') (gaussSum χ (ψ.mulShift (↑(-1) : R))) = gaussSum χ ψ
⊢ HMul.hMul (α := R') ((χ : (a : R) → R') (-1) : R') (gaussSum χ ψ⁻¹) = gaussSum χ ψ

Tactic:
rw [ψ.inv_mulShift, ← Units.coe_neg_one]

Premises used: Units.coe_neg_one, AddChar.inv_mulShift
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
⊢ HMul.hMul (α := R') ((χ : (a : R) → R') (↑(-1) : R) : R') (gaussSum χ (ψ.mulShift (↑(-1) : R))) = gaussSum χ ψ

Tactic:
gaussSum_mulShift χ ψ (-1)

Premises used: OfNat.ofNat, Neg.neg, gaussSum_mulShift
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
⊢ HMul.hMul (α := R') ((χ : (a : R) → R') (↑(-1) : R) : R') (gaussSum χ (ψ.mulShift (↑(-1) : R))) = gaussSum χ ψ

Tactic:
exact gaussSum_mulShift χ ψ (-1)

Premises used: OfNat.ofNat, Neg.neg, gaussSum_mulShift
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
inl :
  ∀ (hb : b = 0),
    Eq.{v + 1} (α := R')
      (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
      (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))
inr :
  ∀ (hb : b ≠ 0),
    Eq.{v + 1} (α := R')
      (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
      (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))
⊢ Eq.{v + 1} (α := R')
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
    (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))

Tactic:
rcases eq_or_ne b 0 with hb | hb

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b = 0
⊢ Eq.{v + 1} (α := R')
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
    (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))

Tactic:
simp only [hb, inv_zero, mul_zero, MulChar.map_zero, zero_mul,
      Finset.sum_const_zero, map_zero_eq_one, mul_one, χ.sum_eq_zero_of_ne_one hχ]

Premises used: inv_zero, MulZeroClass.zero_mul, AddChar.map_zero_eq_one, Finset.sum_const_zero, MulZeroClass.mul_zero, mul_one, MulChar.map_zero, MulChar.sum_eq_zero_of_ne_one
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
⊢ Eq.{v + 1} (α := R')
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
    (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))

Tactic:
(Fintype.sum_bijective _ (mulLeft_bijective₀ b hb) _ _ fun x ↦ ?_).symm

Premises used: mulLeft_bijective₀, Fintype.sum_bijective, Eq.symm
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
inr :
  ∀ (x : R),
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * x * b⁻¹) : R') ((ψ : (a : R) → R') (b * x - b) : R')
⊢ Eq.{v + 1} (α := R')
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
    (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))

Tactic:
refine (Fintype.sum_bijective _ (mulLeft_bijective₀ b hb) _ _ fun x ↦ ?_).symm

Premises used: mulLeft_bijective₀, Fintype.sum_bijective, Eq.symm