awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : R
inr :
  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')
inr₁ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (b⁻¹ * x)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₂ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * b⁻¹ * x) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₃ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (1 * x) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₄ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₅ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * x - b * 1) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₆ inr₇ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * x - b) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * x - b) : 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')

Tactic:
rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel₀ hb, one_mul, mul_sub, mul_one]

Premises used: mul_inv_cancel₀, mul_sub, mul_assoc, mul_comm, mul_one, one_mul
-- 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'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
simp :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ i : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
          HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x⁻¹ : R') ((ψ : (a : R) → R') (-x) : R'))
    (↑(Fintype.card R) : R')
⊢ gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = (↑(Fintype.card R) : R')

Tactic:
simp only [gaussSum, AddChar.inv_apply, Finset.sum_mul, Finset.mul_sum, MulChar.inv_apply']

Premises used: Finset.mul_sum, AddChar.inv_apply, gaussSum, MulChar.inv_apply', Finset.sum_mul
-- 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'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
h :
  ∀ (x y : R),
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') y : R') ((ψ : (a : R) → R') y : R') *
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x⁻¹ : R') ((ψ : (a : R) → R') (-x) : R')
| Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ i : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
          HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x⁻¹ : R') ((ψ : (a : R) → R') (-x) : R'))
    (↑(Fintype.card R) : R')

Tactic:
enter [1, 2, x, 2, y]
-- 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'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
x y : R
h : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (y * x⁻¹) : R') ((ψ : (a : R) → R') (y - x) : R')
| HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') y : R') ((ψ : (a : R) → R') y : R') *
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x⁻¹ : R') ((ψ : (a : R) → R') (-x) : R')

Tactic:
rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]

Premises used: mul_mul_mul_comm, sub_eq_add_neg, AddChar.map_add_eq_mul, map_mul
-- 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'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
h : ∀ (x y : R), HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (y * x⁻¹) : R') ((ψ : (a : R) → R') (y - x) : R')
| Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ i : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
          HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x⁻¹ : R') ((ψ : (a : R) → R') (-x) : R'))
    (↑(Fintype.card R) : R')

Tactic:
enter [1, 2, x, 2, y]
    rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]

Premises used: mul_mul_mul_comm, sub_eq_add_neg, AddChar.map_add_eq_mul, map_mul
-- 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'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
conv :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ y : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (y * x⁻¹) : R') ((ψ : (a : R) → R') (y - x) : R'))
    (↑(Fintype.card R) : R')
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ i : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
          HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x⁻¹ : R') ((ψ : (a : R) → R') (-x) : R'))
    (↑(Fintype.card R) : R')

Tactic:
conv =>
    enter [1, 2, x, 2, y]
    rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]

Premises used: mul_mul_mul_comm, sub_eq_add_neg, AddChar.map_add_eq_mul, map_mul
-- 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'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
simp_rw :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (x * (c - 1)) : R'))
    (↑(Fintype.card R) : R')
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ y : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (y * x⁻¹) : R') ((ψ : (a : R) → R') (y - x) : R'))
    (↑(Fintype.card R) : R')

Tactic:
simp_rw [gaussSum_mul_aux hχ ψ]

Premises used: _private.0.gaussSum_mul_aux
-- 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'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
rw :
  Eq.{v + 1} (α := R')
    (∑ y : R,
      ∑ x : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') y : R') ((ψ : (a : R) → R') (x * (y - 1)) : R'))
    (↑(Fintype.card R) : R')
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (x * (c - 1)) : R'))
    (↑(Fintype.card R) : R')

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- 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'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
simp_rw :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      if x = 1 then HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((↑(Fintype.card R) : R') : R') else 0)
    (↑(Fintype.card R) : R')
⊢ Eq.{v + 1} (α := R')
    (∑ y : R,
      ∑ x : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') y : R') ((ψ : (a : R) → R') (x * (y - 1)) : R'))
    (↑(Fintype.card R) : R')

Tactic:
simp_rw [← Finset.mul_sum, sum_mulShift _ hψ, sub_eq_zero, apply_ite, Nat.cast_zero, mul_zero]

Premises used: Finset.mul_sum, AddChar.sum_mulShift, sub_eq_zero, apply_ite, MulZeroClass.mul_zero, Nat.cast_zero
-- 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'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
rw :
  (if Membership.mem (γ := Finset R) Finset.univ 1 then
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') 1 : R') ((↑(Fintype.card R) : R') : R')
    else 0) =
    (↑(Fintype.card R) : R')
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      if x = 1 then HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((↑(Fintype.card R) : R') : R') else 0)
    (↑(Fintype.card R) : R')

Tactic:
rw [Finset.sum_ite_eq' Finset.univ (1 : R)]

Premises used: Finset.univ, Finset.sum_ite_eq', 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'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
⊢ (if Membership.mem (γ := Finset R) Finset.univ 1 then
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') 1 : R') ((↑(Fintype.card R) : R') : R')
    else 0) =
    (↑(Fintype.card R) : R')

Tactic:
simp only [Finset.mem_univ, map_one, one_mul, if_true]

Premises used: Finset.mem_univ, if_true, map_one, one_mul
-- 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'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
classical :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') (∑ i : R, (ψ : (a : R) → R') (i * (x - 1)) : R'))
    (↑(Fintype.card R) : R')
classical₁ :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R')
        ((↑(if x - 1 = 0 then Fintype.card R else 0) : R') : R'))
    (↑(Fintype.card R) : R')
classical₂ :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((↑(if x = 1 then Fintype.card R else 0) : R') : R'))
    (↑(Fintype.card R) : R')
classical₃ :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      if x = 1 then HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((↑(Fintype.card R) : R') : R')
      else HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((↑0 : R') : R'))
    (↑(Fintype.card R) : R')
classical₄ :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      if x = 1 then HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((↑(Fintype.card R) : R') : R')
      else HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') (0 : R'))
    (↑(Fintype.card R) : R')
classical₅ :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      if x = 1 then HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((↑(Fintype.card R) : R') : R') else 0)
    (↑(Fintype.card R) : R')
classical₆ :
  (if Membership.mem (γ := Finset R) Finset.univ 1 then
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') 1 : R') ((↑(Fintype.card R) : R') : R')
    else 0) =
    (↑(Fintype.card R) : R')
⊢ Eq.{v + 1} (α := R')
    (∑ y : R,
      ∑ x : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') y : R') ((ψ : (a : R) → R') (x * (y - 1)) : R'))
    (↑(Fintype.card R) : R')

Tactic:
classical -- to get `[DecidableEq R]` for `sum_mulShift`
  simp_rw [← Finset.mul_sum, sum_mulShift _ hψ, sub_eq_zero, apply_ite, Nat.cast_zero, mul_zero]
  rw [Finset.sum_ite_eq' Finset.univ (1 : R)]
  simp only [Finset.mem_univ, map_one, one_mul, if_true]

Premises used: Finset.mem_univ, Finset.mul_sum, if_true, sub_eq_zero, apply_ite, MulZeroClass.mul_zero, map_one, Nat.cast_zero, one_mul
-- 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'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
⊢ χ ^ (orderOf χ - 1) = χ⁻¹

Tactic:
(inv_eq_of_mul_eq_one_right ?_).symm

Premises used: inv_eq_of_mul_eq_one_right, 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'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
refine : χ * χ ^ (orderOf χ - 1) = 1
⊢ χ ^ (orderOf χ - 1) = χ⁻¹

Tactic:
refine (inv_eq_of_mul_eq_one_right ?_).symm

Premises used: inv_eq_of_mul_eq_one_right, 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'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
rw : χ ^ (orderOf χ - 1 + 1) = 1
rw₁ : χ ^ orderOf χ = 1
rw₂ rw₃ : Eq (α := MulChar R R') 1 1
⊢ χ * χ ^ (orderOf χ - 1) = 1

Tactic:
rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos, pow_orderOf_eq_one]

Premises used: Nat.sub_one_add_one_eq_of_pos, pow_orderOf_eq_one, MulChar.orderOf_pos, pow_succ'
-- 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'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
⊢ χ ^ (orderOf χ - 1) = χ⁻¹

Tactic:
have h : χ ^ (orderOf χ - 1) = χ⁻¹ := by
    refine (inv_eq_of_mul_eq_one_right ?_).symm
    rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos, pow_orderOf_eq_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'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
h : χ ^ (orderOf χ - 1) = χ⁻¹
rw :
  gaussSum χ ψ * gaussSum χ⁻¹ ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₁ :
  gaussSum χ ψ * HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (-1) : R') (gaussSum χ⁻¹ ψ⁻¹) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₂ :
  HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (-1) : R') (gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₃ :
  HMul.hMul (α := R') (β := R') ((χ⁻¹ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₄ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1)⁻¹ : R') ((↑(Fintype.card R) : R') : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₅ rw₆ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')

Tactic:
rw [h, ← mul_gaussSum_inv_eq_gaussSum χ⁻¹, mul_left_comm, gaussSum_mul_gaussSum_eq_card hχ hψ,
    MulChar.inv_apply', inv_neg_one]

Premises used: mul_gaussSum_inv_eq_gaussSum, mul_left_comm, Inv.inv, MulChar.inv_apply', gaussSum_mul_gaussSum_eq_card, inv_neg_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'
h : Ne.{v + 1} (α := R') (↑(Fintype.card R) : R') 0
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
⊢ gaussSum χ ψ ≠ 0

Tactic:
fun H ↦ h.symm <| zero_mul (gaussSum χ⁻¹ _) ▸ H ▸ gaussSum_mul_gaussSum_eq_card hχ hψ

Premises used: MulZeroClass.zero_mul, Eq.rec, Ne.symm, Inv.inv, gaussSum, Not
-- 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
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
rw : gaussSum χ ψ * gaussSum χ ψ = gaussSum χ ψ * HMul.hMul (β := R') (gaussSum χ ψ⁻¹) ((χ : (a : R) → R') (-1) : R')
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')

Tactic:
rw [pow_two, ← gaussSum_mul_gaussSum_eq_card hχ₁ hψ, hχ₂.inv, mul_rotate']

Premises used: pow_two, MulChar.IsQuadratic.inv, mul_rotate', gaussSum_mul_gaussSum_eq_card
-- 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
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
e_a : gaussSum χ ψ = HMul.hMul (β := R') (gaussSum χ ψ⁻¹) ((χ : (a : R) → R') (-1) : R')
⊢ gaussSum χ ψ * gaussSum χ ψ = gaussSum χ ψ * HMul.hMul (β := R') (gaussSum χ ψ⁻¹) ((χ : (a : R) → R') (-1) : R')

Tactic:
congr
-- 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
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
e_a :
  HMul.hMul (α := R') ((χ : (a : R) → R') (↑(-1) : R) : R') (gaussSum χ (ψ.mulShift (↑(-1) : R))) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (-1) : R') (gaussSum χ (ψ.mulShift (-1)))
⊢ gaussSum χ ψ = HMul.hMul (β := R') (gaussSum χ ψ⁻¹) ((χ : (a : R) → R') (-1) : R')

Tactic:
rw [mul_comm, ← gaussSum_mulShift _ _ (-1 : Rˣ), inv_mulShift]

Premises used: mul_comm, OfNat.ofNat, Neg.neg, AddChar.inv_mulShift, 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
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
⊢ HMul.hMul (α := R') ((χ : (a : R) → R') (↑(-1) : R) : R') (gaussSum χ (ψ.mulShift (↑(-1) : R))) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (-1) : R') (gaussSum χ (ψ.mulShift (-1)))

Tactic:
rfl
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
rw :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      (frobenius R' p : (a : R') → R')
        (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') x : R')))
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ ^ p : (a : R) → R') a : R') ((ψ ^ p : (a : R) → R') a : R'))
⊢ gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p)

Tactic:
rw [← frobenius_def, gaussSum, gaussSum, map_sum]

Premises used: map_sum, frobenius_def, gaussSum
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
simp_rw :
  Eq.{v + 1} (α := R')
    (∑ x : R, HPow.hPow (α := R') ((χ : (a : R) → R') x : R') p * HPow.hPow (α := R') ((ψ : (a : R) → R') x : R') p)
    (∑ x : R, HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') x : R') p) ((ψ ^ p : (a : R) → R') x : R'))
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      (frobenius R' p : (a : R') → R')
        (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') x : R')))
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ ^ p : (a : R) → R') a : R') ((ψ ^ p : (a : R) → R') a : R'))

Tactic:
simp_rw [pow_apply' χ fp.1.ne_zero, map_mul, frobenius_def]

Premises used: MulChar.pow_apply', map_mul, frobenius_def, Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ Eq.{v + 1} (α := R')
    (∑ x : R, HPow.hPow (α := R') ((χ : (a : R) → R') x : R') p * HPow.hPow (α := R') ((ψ : (a : R) → R') x : R') p)
    (∑ x : R, HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') x : R') p) ((ψ ^ p : (a : R) → R') x : R'))

Tactic:
rfl
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
rw : gaussSum (χ ^ p) (ψ ^ p) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
rw₁ : gaussSum (χ ^ p) (ψ.mulShift (↑p : R)) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
rw₂ : gaussSum χ (ψ.mulShift (↑p : R)) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
rw₃ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R')
      (HMul.hMul (α := R') ((χ : (a : R) → R') (↑hp.unit : R) : R') (gaussSum χ (ψ.mulShift (↑hp.unit : R))))
rw₄ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (↑p : R) : R') ((χ : (a : R) → R') (↑hp.unit : R) : R') *
      gaussSum χ (ψ.mulShift (↑hp.unit : R))
rw₅ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (↑p : R) : R') ((χ : (a : R) → R') (↑p : R) : R') *
      gaussSum χ (ψ.mulShift (↑p : R))
rw₆ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑p : R) : R') 2 * gaussSum χ (ψ.mulShift (↑p : R))
rw₇ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') ((HPow.hPow (β := ℕ) χ 2 : (a : R) → R') (↑p : R) : R') (gaussSum χ (ψ.mulShift (↑p : R)))
rw₈ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') ((1 : (a : R) → R') (↑p : R) : R') (gaussSum χ (ψ.mulShift (↑p : R)))
rw₉ :
  gaussSum χ (ψ.mulShift (↑hp.unit : R)) =
    HMul.hMul (α := R') ((1 : (a : R) → R') (↑hp.unit : R) : R') (gaussSum χ (ψ.mulShift (↑hp.unit : R)))
rw₁₀ : gaussSum χ (ψ.mulShift (↑hp.unit : R)) = 1 * gaussSum χ (ψ.mulShift (↑hp.unit : R))
rw₁₁ rw₁₂ : gaussSum χ (ψ.mulShift (↑hp.unit : R)) = gaussSum χ (ψ.mulShift (↑hp.unit : R))
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)

Tactic:
rw [_root_.gaussSum_frob, pow_mulShift, hχ.pow_char p, ← gaussSum_mulShift χ ψ hp.unit,
    ← mul_assoc, hp.unit_spec, ← pow_two, ← pow_apply' _ two_ne_zero, hχ.sq_eq_one, ← hp.unit_spec,
    one_apply_coe, one_mul]

Premises used: MulChar.IsQuadratic.sq_eq_one, pow_two, MulChar.one_apply_coe, mul_assoc, gaussSum_frob, MulChar.IsQuadratic.pow_char, AddChar.pow_mulShift, MulChar.pow_apply', two_ne_zero, IsUnit.unit, IsUnit.unit_spec, one_mul, gaussSum_mulShift
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
zero :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 1 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
zero₁ :
  gaussSum χ ψ = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
zero₂ : gaussSum χ ψ = HMul.hMul (α := R') ((χ : (a : R) → R') 1 : R') (gaussSum χ ψ)
zero₃ : gaussSum χ ψ = 1 * gaussSum χ ψ
zero₄ zero₅ : gaussSum χ ψ = gaussSum χ ψ
⊢ gaussSum χ ψ ^ HPow.hPow (β := ℕ) p 0 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)

Tactic:
rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]

Premises used: MulChar.map_one, pow_zero, pow_one, one_mul