awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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)
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have this : Fact (Nat.Prime (ringChar FF))
Tactic: have := Fact.mk FFp
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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))
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have hFF : ringChar FF ≠ 2
Tactic: have hFF := hchar ▸ hF
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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)
have rw : ¬ringChar FF ∣ 8
Tactic: rw [isUnit_iff_not_dvd_char, ringChar_zmod_n]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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
⊢ ¬ringChar FF ∣ 8
have hFF₁ : ¬ringChar FF ∣ 2
Tactic: rw [Ne, ← Nat.prime_dvd_prime_iff_eq FFp Nat.prime_two] at hFF
Cleared hypotheses: hFF
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have hu : 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
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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)
⊢ Ne.{u_1 + 1} (α := F) (↑(↑8 : ℕ) : F) 0
have h : (↑(↑8 : ℕ) : F) = HPow.hPow (α := F) (β := ℕ) 2 3
Tactic: convert! hp2 3 using 1
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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)
⊢ (↑(↑8 : ℕ) : F) = HPow.hPow (α := F) (β := ℕ) 2 3
have h : Eq.{u_1 + 1} (α := F) 8 (↑(HPow.hPow (α := ℕ) (β := ℕ) 2 3) : F)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
have rw : HPow.hPow (α := FF) (β := ℕ)
    ((ψ₈.char : (a : ZMod (↑8 : ℕ)) → CyclotomicField (↑ψ₈.n : ℕ) F) 1 : CyclotomicField (↑ψ₈.n : ℕ) F) 4 =
  -1
Tactic: rw [show τ = ψ₈.char 1 from rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
have refine_1 : HPow.hPow (β := ℕ)
    (HPow.hPow (α := FF) (β := ℕ)
      ((ψ₈.char : (a : ZMod (↑8 : ℕ)) → CyclotomicField (↑ψ₈.n : ℕ) F) 1 : CyclotomicField (↑ψ₈.n : ℕ) F) 4)
    2 =
  1
Tactic: refine (sq_eq_one_iff.1 ?_).resolve_left ?_
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
⊢ HPow.hPow (α := FF) (β := ℕ)
      ((ψ₈.char : (a : ZMod (↑8 : ℕ)) → CyclotomicField (↑ψ₈.n : ℕ) F) 1 : CyclotomicField (↑ψ₈.n : ℕ) F) 4 =
    -1
have refine_2 : ¬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 ?_
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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 (β := ℕ)
      (HPow.hPow (α := FF) (β := ℕ)
        ((ψ₈.char : (a : ZMod (↑8 : ℕ)) → CyclotomicField (↑ψ₈.n : ℕ) F) 1 : CyclotomicField (↑ψ₈.n : ℕ) F) 4)
      2 =
    1
have refine_1 : HSMul.hSMul (β := ZMod (↑8 : ℕ)) (HMul.hMul (α := ℕ) 4 2) 1 = 0
Tactic: rw [← pow_mul, ← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
have refine_2 : ¬HSMul.hSMul (α := ℕ) (β := ZMod (↑8 : ℕ)) 4 1 = 0
Tactic: rw [← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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 (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have τ_spec : 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
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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)
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
Tactic: have hχ : χ (-1) = 1 := Int.cast_one
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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)
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have hq : χ.IsQuadratic
Tactic: have hq : IsQuadratic χ := isQuadratic_χ₈.comp _
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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)
have 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)
Tactic: ext1
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
⊢ (↑((χ₈ : (a : ZMod 8) → ℤ) x) : FF) * τ ^ (↑x : ℕ) =
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) x : FF) ((ψ₈char : (a : ZMod 8) → FF) x : FF)
have h : τ = IsCyclotomicExtension.zeta (↑8 : ℕ) F (CyclotomicField (↑8 : ℕ) F)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have 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)
Tactic: have h₁ : (fun (a : Fin 8) ↦ ↑(χ₈ a) * τ ^ (a : ℕ)) = fun a ↦ χ a * ↑(ψ₈char a) := by
    ext1; congr; apply pow_one
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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)
⊢ (↑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)
have simp : τ + -1 * HPow.hPow (β := ℕ) τ 3 + -1 * HPow.hPow (β := ℕ) τ 5 + 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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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)
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have hg₁ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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)
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ₈char) 2 =
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) ((↑(Fintype.card (ZMod 8)) : FF) : FF)
have rw : HPow.hPow (β := ℕ) (2 * (τ - HPow.hPow (β := ℕ) τ 3)) 2 = 8
Tactic: rw [hχ, one_mul, ZMod.card, Nat.cast_ofNat, hg₁]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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)
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have hg : HPow.hPow (β := ℕ) (gaussSum χ ψ₈char) 2 =
  HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) ((↑(Fintype.card (ZMod 8)) : FF) : FF)
Tactic: have hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * Fintype.card (ZMod 8) := by
    rw [hχ, one_mul, ZMod.card, Nat.cast_ofNat, hg₁]
    linear_combination (4 * τ ^ 2 - 8) * τ_spec