awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
⊢ IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)

Tactic:
have hu : IsUnit (ringChar FF : ZMod 8) := by
    rw [isUnit_iff_not_dvd_char, ringChar_zmod_n]
    rw [Ne, ← Nat.prime_dvd_prime_iff_eq FFp Nat.prime_two] at hFF
    change ¬_ ∣ 2 ^ 3
    exact mt FFp.dvd_of_dvd_pow hFF
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
⊢ HPow.hPow (α := F) (β := ℕ) 2 3 ≠ 0

Tactic:
hp2 3

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
h : (↑(↑8 : ℕ) : F) = HPow.hPow (α := F) (β := ℕ) 2 3
⊢ Ne.{u_1 + 1} (α := F) (↑(↑8 : ℕ) : F) 0

Tactic:
convert! hp2 3 using 1

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
h h₁ h₂ h₃ : Eq.{u_1 + 1} (α := F) 8 (↑(HPow.hPow (α := ℕ) (β := ℕ) 2 3) : F)
⊢ (↑(↑8 : ℕ) : F) = HPow.hPow (α := F) (β := ℕ) 2 3

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
rw :
  HPow.hPow (α := FF) (β := ℕ)
      ((ψ₈.char : (a : ZMod (↑8 : ℕ)) → CyclotomicField (↑ψ₈.n : ℕ) F) 1 : CyclotomicField (↑ψ₈.n : ℕ) F) 4 =
    -1
⊢ HPow.hPow (β := ℕ) τ 4 = -1

Tactic:
rw [show τ = ψ₈.char 1 from rfl]

Premises used: rfl
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
⊢ HPow.hPow (α := FF) (β := ℕ)
      ((ψ₈.char : (a : ZMod (↑8 : ℕ)) → CyclotomicField (↑ψ₈.n : ℕ) F) 1 : CyclotomicField (↑ψ₈.n : ℕ) F) 4 =
    -1

Tactic:
(sq_eq_one_iff.1 ?_).resolve_left ?_

Premises used: sq_eq_one_iff, Or.resolve_left, Iff.mp
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
refine_1 :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := FF) (β := ℕ)
        ((ψ₈.char : (a : ZMod (↑8 : ℕ)) → CyclotomicField (↑ψ₈.n : ℕ) F) 1 : CyclotomicField (↑ψ₈.n : ℕ) F) 4)
      2 =
    1
refine_2 :
  ¬HPow.hPow (α := FF) (β := ℕ)
        ((ψ₈.char : (a : ZMod (↑8 : ℕ)) → CyclotomicField (↑ψ₈.n : ℕ) F) 1 : CyclotomicField (↑ψ₈.n : ℕ) F) 4 =
      1
⊢ HPow.hPow (α := FF) (β := ℕ)
      ((ψ₈.char : (a : ZMod (↑8 : ℕ)) → CyclotomicField (↑ψ₈.n : ℕ) F) 1 : CyclotomicField (↑ψ₈.n : ℕ) F) 4 =
    -1

Tactic:
refine (sq_eq_one_iff.1 ?_).resolve_left ?_

Premises used: sq_eq_one_iff, Or.resolve_left, Iff.mp
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
refine_1 : HSMul.hSMul (β := ZMod (↑8 : ℕ)) (HMul.hMul (α := ℕ) 4 2) 1 = 0
⊢ HPow.hPow (β := ℕ)
      (HPow.hPow (α := FF) (β := ℕ)
        ((ψ₈.char : (a : ZMod (↑8 : ℕ)) → CyclotomicField (↑ψ₈.n : ℕ) F) 1 : CyclotomicField (↑ψ₈.n : ℕ) F) 4)
      2 =
    1

Tactic:
rw [← pow_mul, ← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]

Premises used: AddChar.map_nsmul_eq_pow, AddChar.IsPrimitive.zmod_char_eq_one_iff, AddChar.PrimitiveAddChar.char, pow_mul, AddChar.PrimitiveAddChar.prim
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
⊢ HSMul.hSMul (β := ZMod (↑8 : ℕ)) (HMul.hMul (α := ℕ) 4 2) 1 = 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
refine_2 : ¬HSMul.hSMul (α := ℕ) (β := ZMod (↑8 : ℕ)) 4 1 = 0
⊢ ¬HPow.hPow (α := FF) (β := ℕ)
        ((ψ₈.char : (a : ZMod (↑8 : ℕ)) → CyclotomicField (↑ψ₈.n : ℕ) F) 1 : CyclotomicField (↑ψ₈.n : ℕ) F) 4 =
      1

Tactic:
rw [← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]

Premises used: AddChar.map_nsmul_eq_pow, AddChar.IsPrimitive.zmod_char_eq_one_iff, AddChar.PrimitiveAddChar.char, AddChar.PrimitiveAddChar.prim
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
⊢ ¬HSMul.hSMul (α := ℕ) (β := ZMod (↑8 : ℕ)) 4 1 = 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
⊢ HPow.hPow (β := ℕ) τ 4 = -1

Tactic:
have τ_spec : τ ^ 4 = -1 := by
    rw [show τ = ψ₈.char 1 from rfl] -- to make `rw [ψ₈.prim.zmod_char_eq_one_iff]` work
    refine (sq_eq_one_iff.1 ?_).resolve_left ?_
    · rw [← pow_mul, ← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]
      decide
    · rw [← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]
      decide
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
⊢ Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)

Tactic:
have hχ : χ (-1) = 1 := Int.cast_one
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
⊢ χ.IsQuadratic

Tactic:
have hq : IsQuadratic χ := isQuadratic_χ₈.comp _
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
h :
  ∀ (x : Fin 8),
    (↑((χ₈ : (a : ZMod 8) → ℤ) x) : FF) * τ ^ (↑x : ℕ) =
      HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) x : FF) ((ψ₈char : (a : ZMod 8) → FF) x : FF)
⊢ Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)

Tactic:
ext1
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
x : Fin 8
h : τ = IsCyclotomicExtension.zeta (↑8 : ℕ) F (CyclotomicField (↑8 : ℕ) F)
⊢ (↑((χ₈ : (a : ZMod 8) → ℤ) x) : FF) * τ ^ (↑x : ℕ) =
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) x : FF) ((ψ₈char : (a : ZMod 8) → FF) x : FF)

Tactic:
congr
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
x : Fin 8
⊢ τ = IsCyclotomicExtension.zeta (↑8 : ℕ) F (CyclotomicField (↑8 : ℕ) F)

Tactic:
apply pow_one

Premises used: pow_one
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
⊢ Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)

Tactic:
have h₁ : (fun (a : Fin 8) ↦ ↑(χ₈ a) * τ ^ (a : ℕ)) = fun a ↦ χ a * ↑(ψ₈char a) := by
    ext1; congr; apply pow_one
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
h₁ :
  Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)
rw :
  (↑0 : FF) * τ ^ (↑0 : ℕ) + (↑1 : FF) * τ ^ (↑1 : ℕ) + (↑0 : FF) * τ ^ (↑2 : ℕ) +
              (↑(-1) : FF) * HPow.hPow (β := ℕ) τ 3 +
            (↑0 : FF) * τ ^ (↑4 : ℕ) +
          (↑(-1) : FF) * HPow.hPow (β := ℕ) τ 5 +
        (↑0 : FF) * τ ^ (↑6 : ℕ) +
      (↑1 : FF) * HPow.hPow (β := ℕ) τ 7 =
    2 * (τ - HPow.hPow (β := ℕ) τ 3)
⊢ gaussSum χ ψ₈char = 2 * (τ - HPow.hPow (β := ℕ) τ 3)

Tactic:
rw [gaussSum, ← h₁, Fin.sum_univ_eight,
      -- evaluate `χ₈`
      show χ₈ 0 = 0 from rfl, show χ₈ 1 = 1 from rfl, show χ₈ 2 = 0 from rfl,
      show χ₈ 3 = -1 from rfl, show χ₈ 4 = 0 from rfl, show χ₈ 5 = -1 from rfl,
      show χ₈ 6 = 0 from rfl, show χ₈ 7 = 1 from rfl,
      -- normalize exponents
      show ((3 : Fin 8) : ℕ) = 3 from rfl, show ((5 : Fin 8) : ℕ) = 5 from rfl,
      show ((7 : Fin 8) : ℕ) = 7 from rfl]

Premises used: Fin.sum_univ_eight, gaussSum, rfl
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
h₁ :
  Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)
simp :
  τ + -1 * HPow.hPow (β := ℕ) τ 3 + -1 * HPow.hPow (β := ℕ) τ 5 + HPow.hPow (β := ℕ) τ 7 =
    2 * (τ - HPow.hPow (β := ℕ) τ 3)
⊢ (↑0 : FF) * τ ^ (↑0 : ℕ) + (↑1 : FF) * τ ^ (↑1 : ℕ) + (↑0 : FF) * τ ^ (↑2 : ℕ) +
              (↑(-1) : FF) * HPow.hPow (β := ℕ) τ 3 +
            (↑0 : FF) * τ ^ (↑4 : ℕ) +
          (↑(-1) : FF) * HPow.hPow (β := ℕ) τ 5 +
        (↑0 : FF) * τ ^ (↑6 : ℕ) +
      (↑1 : FF) * HPow.hPow (β := ℕ) τ 7 =
    2 * (τ - HPow.hPow (β := ℕ) τ 3)

Tactic:
simp only [Int.cast_zero, zero_mul, Int.cast_one, Fin.val_one, pow_one, one_mul, zero_add,
      Fin.val_two, add_zero, Int.reduceNeg, Int.cast_neg]

Premises used: Fin.val_two, Int.cast_neg, Int.cast_zero, Int.reduceNeg, MulZeroClass.zero_mul, Fin.val_one, zero_add, pow_one, add_zero, one_mul, Int.cast_one
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
h₁ :
  Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)
⊢ τ + -1 * HPow.hPow (β := ℕ) τ 3 + -1 * HPow.hPow (β := ℕ) τ 5 + HPow.hPow (β := ℕ) τ 7 =
    2 * (τ - HPow.hPow (β := ℕ) τ 3)

Tactic:
linear_combination (τ ^ 3 - τ) * τ_spec

Premises used: HSub.hSub, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
h₁ :
  Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)
⊢ gaussSum χ ψ₈char = 2 * (τ - HPow.hPow (β := ℕ) τ 3)

Tactic:
have hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3) := by
    rw [gaussSum, ← h₁, Fin.sum_univ_eight,
      -- evaluate `χ₈`
      show χ₈ 0 = 0 from rfl, show χ₈ 1 = 1 from rfl, show χ₈ 2 = 0 from rfl,
      show χ₈ 3 = -1 from rfl, show χ₈ 4 = 0 from rfl, show χ₈ 5 = -1 from rfl,
      show χ₈ 6 = 0 from rfl, show χ₈ 7 = 1 from rfl,
      -- normalize exponents
      show ((3 : Fin 8) : ℕ) = 3 from rfl, show ((5 : Fin 8) : ℕ) = 5 from rfl,
      show ((7 : Fin 8) : ℕ) = 7 from rfl]
    simp only [Int.cast_zero, zero_mul, Int.cast_one, Fin.val_one, pow_one, one_mul, zero_add,
      Fin.val_two, add_zero, Int.reduceNeg, Int.cast_neg]
    linear_combination (τ ^ 3 - τ) * τ_spec
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
h₁ :
  Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)
hg₁ : gaussSum χ ψ₈char = 2 * (τ - HPow.hPow (β := ℕ) τ 3)
rw : HPow.hPow (β := ℕ) (2 * (τ - HPow.hPow (β := ℕ) τ 3)) 2 = 8
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ₈char) 2 =
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) ((↑(Fintype.card (ZMod 8)) : FF) : FF)

Tactic:
rw [hχ, one_mul, ZMod.card, Nat.cast_ofNat, hg₁]

Premises used: Nat.cast_ofNat, one_mul, ZMod.card