awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
succ :
  gaussSum χ ψ ^ (p ^ n * p) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₁ :
  (gaussSum χ ψ ^ p ^ n) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₂ :
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₃ :
  HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p * gaussSum χ ψ ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₄ :
  HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p *
      HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₅ :
  HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p)
        ((χ : (a : R) → R') (↑p : R) : R') *
      gaussSum χ ψ =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₆ :
  HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p)
        ((χ : (a : R) → R') (↑p : R) : R') *
      gaussSum χ ψ =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n * (↑p : R)) : R') (gaussSum χ ψ)
succ₇ :
  HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p)
        ((χ : (a : R) → R') (↑p : R) : R') *
      gaussSum χ ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R')
        ((χ : (a : R) → R') (↑p : R) : R') *
      gaussSum χ ψ
⊢ gaussSum χ ψ ^ p ^ (n + 1) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
have succ₈ : HMul.hMul (α := R') (β := R') ((χ ^ p : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R')
      ((χ : (a : R) → R') (↑p : R) : R') *
    gaussSum χ ψ =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R')
      ((χ : (a : R) → R') (↑p : R) : R') *
    gaussSum χ ψ
Tactic: 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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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'
⊢ gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
have zero : gaussSum χ ψ ^ HPow.hPow (β := ℕ) p 0 =
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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 χ ψ)
⊢ gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
have 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 χ ψ)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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
⊢ False
have hg₁ : 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
Cleared hypotheses: hg, hf
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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')
⊢ 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)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
⊢ 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)
have rw : HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) = (χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n)
Tactic: rw [← hg]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) = (χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n)
have apply : HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) * gaussSum χ ψ =
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
Tactic: apply mul_right_cancel₀ this
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) * gaussSum χ ψ =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
have rw : HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) * gaussSum χ ψ = gaussSum χ ψ ^ p ^ n
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) * gaussSum χ ψ =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
have rw₁ : gaussSum χ ψ ^ (2 * (p ^ n / 2)) * gaussSum χ ψ = gaussSum χ ψ ^ p ^ n
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) * gaussSum χ ψ =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
have rw₂ : gaussSum χ ψ ^ (2 * (p ^ n / 2) + 1) = gaussSum χ ψ ^ p ^ n
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 ^ (p ^ n / 2) * gaussSum χ ψ =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
have rw₃ : gaussSum χ ψ ^ p ^ n = gaussSum χ ψ ^ p ^ n
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]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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 : ℕ)
⊢ 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)
have 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)
Tactic: obtain ⟨n', hp', hc'⟩ := FiniteField.card F' (ringChar F')
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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'
⊢ 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)
have hchar : ringChar F' = ringChar FF'
Tactic: have hchar := Algebra.ringChar_eq F' FF'
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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'
⊢ 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)
have 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')
Tactic: apply (algebraMap F' FF').injective
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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'
⊢ 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')
have 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' : ℕ)))
Tactic: rw [map_pow, map_mul, map_natCast, hc', hchar, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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'
⊢ 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' : ℕ)))
have 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' : ℕ))
Tactic: simp only [← MulChar.ringHomComp_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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'
⊢ 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' : ℕ))
have this : Fact (Nat.Prime (ringChar F'))
Tactic: have := Fact.mk hp'
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
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'))
⊢ 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' : ℕ))
have this₁ : Fact (Nat.Prime (ringChar FF'))
Tactic: have := Fact.mk (hchar.subst hp')
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
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'))
⊢ 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' : ℕ))
have 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' : ℕ))
Tactic: rw [Ne, ← Nat.prime_dvd_prime_iff_eq hp' hp, ← isUnit_iff_not_dvd_char, hchar] at hch₁
Cleared hypotheses: hch₂, n, hp, hc, n', hp', hc', ψ, FF', hchar, this_1, this
-- 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
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
Tactic: have hp2 (n : ℕ) : (2 ^ n : F) ≠ 0 := pow_ne_zero n (Ring.two_ne_zero 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
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have 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)
Tactic: obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)
-- 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
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have hchar : ringChar F = ringChar FF
Tactic: have hchar := Algebra.ringChar_eq F FF
-- 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
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have FFp : Nat.Prime (ringChar FF)
Tactic: have FFp := hchar.subst hp