awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
n : ℕ
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
zero :
  gaussSum χ ψ ^ HPow.hPow (β := ℕ) p 0 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
succ :
  ∀ (n : ℕ)
    (ih :
      gaussSum χ ψ ^ p ^ n =
        HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)),
    gaussSum χ ψ ^ p ^ (n + 1) =
      HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)

Tactic:
induction n with
  | zero => rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]
  | succ n ih =>
    rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
      ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]

Premises used: MulChar.map_one, pow_succ, mul_assoc, MulChar.IsQuadratic.pow_char, MulChar.pow_apply', Nat.cast, pow_mul, pow_zero, map_mul, HPow.hPow, pow_one, Nat.Prime.ne_zero, MulChar.IsQuadratic.gaussSum_frob, mul_pow, one_mul, Fact.out
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
hp' : p ≠ 2
hg :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
hf : gaussSum χ ψ = 0
⊢ Eq.{v + 1} (α := R') ((χ : (a : R) → R') (-1) : R') (0 : R') ∨ Eq.{v + 1} (α := R') (↑(Fintype.card R) : R') 0

Tactic:
rw [hf, zero_pow two_ne_zero, eq_comm, mul_eq_zero] at hg

Premises used: eq_comm, mul_eq_zero, two_ne_zero, zero_pow
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
hp' : p ≠ 2
hg :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
hf : gaussSum χ ψ = 0
hg₁ : Eq.{v + 1} (α := R') ((χ : (a : R) → R') (-1) : R') (0 : R') ∨ Eq.{v + 1} (α := R') (↑(Fintype.card R) : R') 0
⊢ gaussSum χ ψ = 0

Tactic:
rw [hf, zero_pow two_ne_zero, eq_comm, mul_eq_zero] at hg

Premises used: eq_comm, mul_eq_zero, two_ne_zero, zero_pow
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
hp' : p ≠ 2
hg : Eq.{v + 1} (α := R') ((χ : (a : R) → R') (-1) : R') (0 : R') ∨ Eq.{v + 1} (α := R') (↑(Fintype.card R) : R') 0
hf : gaussSum χ ψ = 0
⊢ False

Tactic:
not_isUnit_prime_of_dvd_card
        ((CharP.cast_eq_zero_iff R' p _).mp <| hg.resolve_left (isUnit_one.neg.map χ).ne_zero) hp

Premises used: not_isUnit_prime_of_dvd_card, Or.resolve_left, isUnit_one, Iff.mp, IsUnit.ne_zero, IsUnit.map, IsUnit.neg, CharP.cast_eq_zero_iff
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
hp' : p ≠ 2
hg : Eq.{v + 1} (α := R') ((χ : (a : R) → R') (-1) : R') (0 : R') ∨ Eq.{v + 1} (α := R') (↑(Fintype.card R) : R') 0
hf : gaussSum χ ψ = 0
⊢ False

Tactic:
exact not_isUnit_prime_of_dvd_card
        ((CharP.cast_eq_zero_iff R' p _).mp <| hg.resolve_left (isUnit_one.neg.map χ).ne_zero) hp

Premises used: not_isUnit_prime_of_dvd_card, Or.resolve_left, isUnit_one, Iff.mp, IsUnit.ne_zero, IsUnit.map, IsUnit.neg, CharP.cast_eq_zero_iff
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
hp' : p ≠ 2
hg :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
⊢ gaussSum χ ψ ≠ 0

Tactic:
have : gaussSum χ ψ ≠ 0 := by
    intro hf
    rw [hf, zero_pow two_ne_zero, eq_comm, mul_eq_zero] at hg
    exact not_isUnit_prime_of_dvd_card
        ((CharP.cast_eq_zero_iff R' p _).mp <| hg.resolve_left (isUnit_one.neg.map χ).ne_zero) hp
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
hp' : p ≠ 2
hg :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
this : gaussSum χ ψ ≠ 0
rw : HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) = (χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n)
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R') ^ (p ^ n / 2) =
    (χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n)

Tactic:
rw [← hg]
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
hp' : p ≠ 2
hg :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
this : gaussSum χ ψ ≠ 0
apply :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) * gaussSum χ ψ =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) = (χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n)

Tactic:
apply mul_right_cancel₀ this

Premises used: mul_right_cancel₀
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
hp' : p ≠ 2
hg :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
this : gaussSum χ ψ ≠ 0
rw : HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) * gaussSum χ ψ = gaussSum χ ψ ^ p ^ n
rw₁ : gaussSum χ ψ ^ (2 * (p ^ n / 2)) * gaussSum χ ψ = gaussSum χ ψ ^ p ^ n
rw₂ : gaussSum χ ψ ^ (2 * (p ^ n / 2) + 1) = gaussSum χ ψ ^ p ^ n
rw₃ rw₄ : gaussSum χ ψ ^ p ^ n = gaussSum χ ψ ^ p ^ n
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) * gaussSum χ ψ =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)

Tactic:
rw [← hχ.gaussSum_frob_iter p n hp ψ, ← pow_mul, ← pow_succ,
    Nat.two_mul_div_two_add_one_of_odd (fp.1.eq_two_or_odd'.resolve_left hp').pow]

Premises used: pow_succ, Nat.two_mul_div_two_add_one_of_odd, Or.resolve_left, MulChar.IsQuadratic.gaussSum_frob_iter, pow_mul, Nat.Prime.eq_two_or_odd', Odd.pow, Fact.out
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
F' : Type u_2
inst_2 : Field F'
inst_3 : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
obtain :
  ∀ (n : ℕ+) (hp : Nat.Prime (ringChar F)) (hc : Fintype.card F = ringChar F ^ (↑n : ℕ)),
    HMul.hMul (α := F') (β := F') ((χ : (a : F) → F') (-1) : F') ((↑(Fintype.card F) : F') : F') ^
        (Fintype.card F' / 2) =
      (χ : (a : F) → F') (↑(Fintype.card F') : F)
⊢ HMul.hMul (α := F') (β := F') ((χ : (a : F) → F') (-1) : F') ((↑(Fintype.card F) : F') : F') ^ (Fintype.card F' / 2) =
    (χ : (a : F) → F') (↑(Fintype.card F') : F)

Tactic:
obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)

Premises used: FiniteField.card, ringChar
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
F' : Type u_2
inst_2 : Field F'
inst_3 : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
obtain :
  ∀ (n' : ℕ+) (hp' : Nat.Prime (ringChar F')) (hc' : Fintype.card F' = ringChar F' ^ (↑n' : ℕ)),
    HMul.hMul (α := F') (β := F') ((χ : (a : F) → F') (-1) : F') ((↑(Fintype.card F) : F') : F') ^
        (Fintype.card F' / 2) =
      (χ : (a : F) → F') (↑(Fintype.card F') : F)
⊢ HMul.hMul (α := F') (β := F') ((χ : (a : F) → F') (-1) : F') ((↑(Fintype.card F) : F') : F') ^ (Fintype.card F' / 2) =
    (χ : (a : F) → F') (↑(Fintype.card F') : F)

Tactic:
obtain ⟨n', hp', hc'⟩ := FiniteField.card F' (ringChar F')

Premises used: FiniteField.card, ringChar
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
F' : Type u_2
inst_2 : Field F'
inst_3 : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ (↑n' : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
⊢ ringChar F' = ringChar FF'

Tactic:
have hchar := Algebra.ringChar_eq F' FF'
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
F' : Type u_2
inst_2 : Field F'
inst_3 : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ (↑n' : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
hchar : ringChar F' = ringChar FF'
a :
  Eq (α := FF')
    (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
        (HMul.hMul (α := F') (β := F') ((χ : (a : F) → F') (-1) : F') ((↑(Fintype.card F) : F') : F') ^
          (Fintype.card F' / 2)) :
      FF')
    (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') ((χ : (a : F) → F') (↑(Fintype.card F') : F)) : FF')
⊢ HMul.hMul (α := F') (β := F') ((χ : (a : F) → F') (-1) : F') ((↑(Fintype.card F) : F') : F') ^ (Fintype.card F' / 2) =
    (χ : (a : F) → F') (↑(Fintype.card F') : F)

Tactic:
apply (algebraMap F' FF').injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
F' : Type u_2
inst_2 : Field F'
inst_3 : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ (↑n' : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
hchar : ringChar F' = ringChar FF'
a :
  HMul.hMul (α := FF') (β := FF') (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') ((χ : (a : F) → F') (-1)) : FF')
        ((↑(Fintype.card F) : FF') : FF') ^
      (ringChar FF' ^ (↑n' : ℕ) / 2) =
    ((algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
      ((χ : (a : F) → F') (HPow.hPow (α := F) (↑(ringChar FF') : F) (↑n' : ℕ)))
⊢ Eq (α := FF')
    (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
        (HMul.hMul (α := F') (β := F') ((χ : (a : F) → F') (-1) : F') ((↑(Fintype.card F) : F') : F') ^
          (Fintype.card F' / 2)) :
      FF')
    (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') ((χ : (a : F) → F') (↑(Fintype.card F') : F)) : FF')

Tactic:
rw [map_pow, map_mul, map_natCast, hc', hchar, Nat.cast_pow]

Premises used: map_pow, map_mul, map_natCast, Nat.cast_pow
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
F' : Type u_2
inst_2 : Field F'
inst_3 : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ (↑n' : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
hchar : ringChar F' = ringChar FF'
a :
  HMul.hMul (α := FF') ((χ.ringHomComp (algebraMap F' FF') : (a : F) → FF') (-1)) (↑(Fintype.card F) : FF') ^
      (ringChar FF' ^ (↑n' : ℕ) / 2) =
    (χ.ringHomComp (algebraMap F' FF') : (a : F) → FF') (HPow.hPow (α := F) (↑(ringChar FF') : F) (↑n' : ℕ))
⊢ HMul.hMul (α := FF') (β := FF') (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') ((χ : (a : F) → F') (-1)) : FF')
        ((↑(Fintype.card F) : FF') : FF') ^
      (ringChar FF' ^ (↑n' : ℕ) / 2) =
    ((algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
      ((χ : (a : F) → F') (HPow.hPow (α := F) (↑(ringChar FF') : F) (↑n' : ℕ)))

Tactic:
simp only [← MulChar.ringHomComp_apply]

Premises used: MulChar.ringHomComp_apply
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
F' : Type u_2
inst_2 : Field F'
inst_3 : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ (↑n' : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
hchar : ringChar F' = ringChar FF'
⊢ Fact (Nat.Prime (ringChar F'))

Tactic:
have := Fact.mk hp'
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
F' : Type u_2
inst_2 : Field F'
inst_3 : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ (↑n' : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
hchar : ringChar F' = ringChar FF'
this : Fact (Nat.Prime (ringChar F'))
⊢ Fact (Nat.Prime (ringChar FF'))

Tactic:
have := Fact.mk (hchar.subst hp')
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
F' : Type u_2
inst_2 : Field F'
inst_3 : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ (↑n' : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
hchar : ringChar F' = ringChar FF'
this_1 : Fact (Nat.Prime (ringChar F'))
this : Fact (Nat.Prime (ringChar FF'))
a :
  ∀ (hch₂ : ringChar F' ≠ 2) (n : ℕ+) (hp : Nat.Prime (ringChar F)) (hc : Fintype.card F = ringChar F ^ (↑n : ℕ))
    (n' : ℕ+) (hp' : Nat.Prime (ringChar F')) (hc' : Fintype.card F' = ringChar F' ^ (↑n' : ℕ)),
    let ψ := FiniteField.primitiveChar F F' hch₁;
    let FF' := CyclotomicField (↑ψ.n : ℕ) F';
    ∀ (hch₁ : IsUnit.{u_1} (M := F) (↑(ringChar FF') : F)) (hchar : ringChar F' = ringChar FF')
      (this : Fact (Nat.Prime (ringChar F'))) (this : Fact (Nat.Prime (ringChar FF'))),
      HMul.hMul (α := FF') ((χ.ringHomComp (algebraMap F' FF') : (a : F) → FF') (-1)) (↑(Fintype.card F) : FF') ^
          (ringChar FF' ^ (↑n' : ℕ) / 2) =
        (χ.ringHomComp (algebraMap F' FF') : (a : F) → FF') (HPow.hPow (α := F) (↑(ringChar FF') : F) (↑n' : ℕ))
⊢ HMul.hMul (α := FF') ((χ.ringHomComp (algebraMap F' FF') : (a : F) → FF') (-1)) (↑(Fintype.card F) : FF') ^
      (ringChar FF' ^ (↑n' : ℕ) / 2) =
    (χ.ringHomComp (algebraMap F' FF') : (a : F) → FF') (HPow.hPow (α := F) (↑(ringChar FF') : F) (↑n' : ℕ))

Tactic:
rw [Ne, ← Nat.prime_dvd_prime_iff_eq hp' hp, ← isUnit_iff_not_dvd_char, hchar] at hch₁

Premises used: Nat.prime_dvd_prime_iff_eq, Ne, isUnit_iff_not_dvd_char
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
F' : Type u_2
inst_2 : Field F'
inst_3 : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁_1 : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ (↑n' : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁_1
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
hch₁ : IsUnit.{u_1} (M := F) (↑(ringChar FF') : F)
hchar : ringChar F' = ringChar FF'
this_1 : Fact (Nat.Prime (ringChar F'))
this : Fact (Nat.Prime (ringChar FF'))
⊢ HMul.hMul (α := FF') ((χ.ringHomComp (algebraMap F' FF') : (a : F) → FF') (-1)) (↑(Fintype.card F) : FF') ^
      (ringChar FF' ^ (↑n' : ℕ) / 2) =
    (χ.ringHomComp (algebraMap F' FF') : (a : F) → FF') (HPow.hPow (α := F) (↑(ringChar FF') : F) (↑n' : ℕ))

Tactic:
Char.card_pow_char_pow (hχ₂.comp _) ψ.char (ringChar FF') n' hch₁ (hchar ▸ hch₂)
       (gaussSum_sq ((ringHomComp_ne_one_iff (RingHom.injective _)).mpr hχ₁) (hχ₂.comp _) ψ.prim)

Premises used: PNat.val, Iff.mpr, MulChar.IsQuadratic.comp, Char.card_pow_char_pow, MulChar.ringHomComp_ne_one_iff, Eq.rec, AddChar.PrimitiveAddChar.char, AddChar.PrimitiveAddChar.prim, ringChar, gaussSum_sq
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
F' : Type u_2
inst_2 : Field F'
inst_3 : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁_1 : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ (↑n' : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁_1
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
hch₁ : IsUnit.{u_1} (M := F) (↑(ringChar FF') : F)
hchar : ringChar F' = ringChar FF'
this_1 : Fact (Nat.Prime (ringChar F'))
this : Fact (Nat.Prime (ringChar FF'))
⊢ HMul.hMul (α := FF') ((χ.ringHomComp (algebraMap F' FF') : (a : F) → FF') (-1)) (↑(Fintype.card F) : FF') ^
      (ringChar FF' ^ (↑n' : ℕ) / 2) =
    (χ.ringHomComp (algebraMap F' FF') : (a : F) → FF') (HPow.hPow (α := F) (↑(ringChar FF') : F) (↑n' : ℕ))

Tactic:
exact Char.card_pow_char_pow (hχ₂.comp _) ψ.char (ringChar FF') n' hch₁ (hchar ▸ hch₂)
       (gaussSum_sq ((ringHomComp_ne_one_iff (RingHom.injective _)).mpr hχ₁) (hχ₂.comp _) ψ.prim)

Premises used: PNat.val, Iff.mpr, MulChar.IsQuadratic.comp, Char.card_pow_char_pow, MulChar.ringHomComp_ne_one_iff, Eq.rec, AddChar.PrimitiveAddChar.char, AddChar.PrimitiveAddChar.prim, ringChar, gaussSum_sq
-- Module: Mathlib.NumberTheory.GaussSum
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
⊢ ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0

Tactic:
have hp2 (n : ℕ) : (2 ^ n : F) ≠ 0 := pow_ne_zero n (Ring.two_ne_zero hF)
-- 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
obtain :
  ∀ (n : ℕ+) (hp : Nat.Prime (ringChar F)) (hc : Fintype.card F = ringChar F ^ (↑n : ℕ)),
    HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)

Tactic:
obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)

Premises used: FiniteField.card, ringChar
-- 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
⊢ ringChar F = ringChar FF

Tactic:
have hchar := Algebra.ringChar_eq F FF
-- 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
⊢ Nat.Prime (ringChar FF)

Tactic:
have FFp := hchar.subst hp
-- 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)
⊢ Fact (Nat.Prime (ringChar FF))

Tactic:
have := Fact.mk FFp
-- 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))
⊢ ringChar FF ≠ 2

Tactic:
have hFF := hchar ▸ hF
-- 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
rw : ¬ringChar FF ∣ 8
⊢ IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)

Tactic:
rw [isUnit_iff_not_dvd_char, ringChar_zmod_n]

Premises used: isUnit_iff_not_dvd_char, ZMod.ringChar_zmod_n
-- 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
⊢ ¬ringChar FF ∣ 2

Tactic:
rw [Ne, ← Nat.prime_dvd_prime_iff_eq FFp Nat.prime_two] at hFF

Premises used: Nat.prime_dvd_prime_iff_eq, Ne, Nat.prime_two
-- 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
⊢ ¬ringChar FF ∣ HPow.hPow (α := ℕ) (β := ℕ) 2 3

Tactic:
mt FFp.dvd_of_dvd_pow hFF

Premises used: Nat.Prime.dvd_of_dvd_pow, mt
-- 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
⊢ ¬ringChar FF ∣ HPow.hPow (α := ℕ) (β := ℕ) 2 3

Tactic:
exact mt FFp.dvd_of_dvd_pow hFF

Premises used: Nat.Prime.dvd_of_dvd_pow, mt