awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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')
⊢ 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')
have 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')
Tactic: rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel₀ hb, one_mul, mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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') ψ
⊢ gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = (↑(Fintype.card R) : R')
have 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')
Tactic: simp only [gaussSum, AddChar.inv_apply, Finset.sum_mul, Finset.mul_sum, MulChar.inv_apply']
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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') ψ
| 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')
have 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')
Tactic: enter [1, 2, x, 2, y]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
| 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')
have h : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (y * x⁻¹) : R') ((ψ : (a : R) → R') (y - x) : R')
Tactic: rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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') ψ
| 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')
have h : ∀ (x y : R), HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (y * x⁻¹) : R') ((ψ : (a : R) → R') (y - x) : R')
Tactic: enter [1, 2, x, 2, y]
    rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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') ψ
⊢ 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')
have 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')
Tactic: conv =>
    enter [1, 2, x, 2, y]
    rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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') ψ
⊢ 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')
have 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')
Tactic: simp_rw [gaussSum_mul_aux hχ ψ]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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') ψ
⊢ 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')
have 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')
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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') ψ
⊢ 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')
have 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')
Tactic: simp_rw [← Finset.mul_sum, sum_mulShift _ hψ, sub_eq_zero, apply_ite, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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') ψ
⊢ 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')
have 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')
Tactic: rw [Finset.sum_ite_eq' Finset.univ (1 : R)]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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') ψ
⊢ 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')
have 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')
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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')
⊢ 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')
have 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')
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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')
⊢ 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')
have 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')
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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')
⊢ 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')
have 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')
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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')
⊢ 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')
have 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')
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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')
⊢ 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')
have 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')
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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')
⊢ 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')
have 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')
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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) = χ⁻¹
have refine : χ * χ ^ (orderOf χ - 1) = 1
Tactic: refine (inv_eq_of_mul_eq_one_right ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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) = 1
have rw : χ ^ (orderOf χ - 1 + 1) = 1
Tactic: rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
⊢ χ * χ ^ (orderOf χ - 1) = 1
have rw₁ : χ ^ orderOf χ = 1
Tactic: rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
⊢ χ * χ ^ (orderOf χ - 1) = 1
have rw₂ : Eq (α := MulChar R R') 1 1
Tactic: rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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') ψ
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
have h : χ ^ (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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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) = χ⁻¹
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
have rw : gaussSum χ ψ * gaussSum χ⁻¹ ψ =
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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')
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
have 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')
Tactic: rw [h, ← mul_gaussSum_inv_eq_gaussSum χ⁻¹, mul_left_comm, gaussSum_mul_gaussSum_eq_card hχ hψ,
    MulChar.inv_apply', inv_neg_one]