[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ ↑χ ↑a * gaussSum χ (mulShift ψ ↑a) = gaussSum χ ψ
[PROOFSTEP]
simp only [gaussSum, mulShift_apply, Finset.mul_sum]
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ ∑ x : R, ↑χ ↑a * (↑χ x * ↑ψ (↑a * x)) = ∑ x : R, ↑χ x * ↑ψ x
[PROOFSTEP]
simp_rw [← mul_assoc, ← map_mul]
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ ∑ x : R, ↑χ (↑a * x) * ↑ψ (↑a * x) = ∑ x : R, ↑χ x * ↑ψ x
[PROOFSTEP]
exact Fintype.sum_bijective _ a.mulLeft_bijective _ _ fun x => rfl
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
b : R
⊢ ∑ a : R, ↑χ (a * b⁻¹) * ↑ψ (a - b) = ∑ c : R, ↑χ c * ↑ψ (b * (c - 1))
[PROOFSTEP]
cases' eq_or_ne b 0 with hb hb
[GOAL]
case inl
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
b : R
hb : b = 0
⊢ ∑ a : R, ↑χ (a * b⁻¹) * ↑ψ (a - b) = ∑ c : R, ↑χ c * ↑ψ (b * (c - 1))
[PROOFSTEP]
simp only [hb, inv_zero, mul_zero, MulChar.map_zero, zero_mul, Finset.sum_const_zero, map_zero_one, mul_one]
[GOAL]
case inl
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
b : R
hb : b = 0
⊢ 0 = ∑ x : R, ↑χ x
[PROOFSTEP]
exact (hχ.sum_eq_zero).symm
[GOAL]
case inr
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
b : R
hb : b ≠ 0
⊢ ∑ a : R, ↑χ (a * b⁻¹) * ↑ψ (a - b) = ∑ c : R, ↑χ c * ↑ψ (b * (c - 1))
[PROOFSTEP]
refine' (Fintype.sum_bijective _ (mulLeft_bijective₀ b hb) _ _ fun x => _).symm
[GOAL]
case inr
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
b : R
hb : b ≠ 0
x : R
⊢ ↑χ x * ↑ψ (b * (x - 1)) = ↑χ ((fun x x_1 => x * x_1) b x * b⁻¹) * ↑ψ ((fun x x_1 => x * x_1) b x - b)
[PROOFSTEP]
rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel hb, one_mul, mul_sub, mul_one]
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card R)
[PROOFSTEP]
simp only [gaussSum, AddChar.inv_apply, Finset.sum_mul, Finset.mul_sum, MulChar.inv_apply']
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ ∑ x : R, ∑ x_1 : R, ↑χ x_1 * ↑ψ x_1 * (↑χ x⁻¹ * ↑ψ (-x)) = ↑(Fintype.card R)
[PROOFSTEP]
conv =>
  lhs; congr; next => skip
  ext; congr; next => skip
  ext
  rw [mul_mul_mul_comm, ← map_mul, ← map_add_mul, ← sub_eq_add_neg]
    --  conv in _ * _ * (_ * _) => rw [mul_mul_mul_comm, ← map_mul, ← map_add_mul, ← sub_eq_add_neg]
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
| ∑ x : R, ∑ x_1 : R, ↑χ x_1 * ↑ψ x_1 * (↑χ x⁻¹ * ↑ψ (-x)) = ↑(Fintype.card R)
[PROOFSTEP]
  lhs; congr; next => skip
  ext; congr; next => skip
  ext
  rw [mul_mul_mul_comm, ← map_mul, ← map_add_mul, ← sub_eq_add_neg]
    --  conv in _ * _ * (_ * _) => rw [mul_mul_mul_comm, ← map_mul, ← map_add_mul, ← sub_eq_add_neg]
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
| ∑ x : R, ∑ x_1 : R, ↑χ x_1 * ↑ψ x_1 * (↑χ x⁻¹ * ↑ψ (-x)) = ↑(Fintype.card R)
[PROOFSTEP]
  lhs; congr; next => skip
  ext; congr; next => skip
  ext
  rw [mul_mul_mul_comm, ← map_mul, ← map_add_mul, ← sub_eq_add_neg]
    --  conv in _ * _ * (_ * _) => rw [mul_mul_mul_comm, ← map_mul, ← map_add_mul, ← sub_eq_add_neg]
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
| ∑ x : R, ∑ x_1 : R, ↑χ x_1 * ↑ψ x_1 * (↑χ x⁻¹ * ↑ψ (-x)) = ↑(Fintype.card R)
[PROOFSTEP]
lhs
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
| ∑ x : R, ∑ x_1 : R, ↑χ x_1 * ↑ψ x_1 * (↑χ x⁻¹ * ↑ψ (-x))
[PROOFSTEP]
congr
[GOAL]
case s
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
| Finset.univ
case f
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
| fun x => ∑ x_1 : R, ↑χ x_1 * ↑ψ x_1 * (↑χ x⁻¹ * ↑ψ (-x))
[PROOFSTEP]
next => skip
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
| Finset.univ
[PROOFSTEP]
skip
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
| Finset.univ
[PROOFSTEP]
skip
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
| Finset.univ
[PROOFSTEP]
skip
[GOAL]
case f
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
| fun x => ∑ x_1 : R, ↑χ x_1 * ↑ψ x_1 * (↑χ x⁻¹ * ↑ψ (-x))
[PROOFSTEP]
ext
[GOAL]
case f.h
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
x✝ : R
| ∑ x : R, ↑χ x * ↑ψ x * (↑χ x✝⁻¹ * ↑ψ (-x✝))
[PROOFSTEP]
congr
[GOAL]
case f.h.s
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
x✝ : R
| Finset.univ
case f.h.f
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
x✝ : R
| fun x => ↑χ x * ↑ψ x * (↑χ x✝⁻¹ * ↑ψ (-x✝))
[PROOFSTEP]
next => skip
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
x✝ : R
| Finset.univ
[PROOFSTEP]
skip
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
x✝ : R
| Finset.univ
[PROOFSTEP]
skip
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
x✝ : R
| Finset.univ
[PROOFSTEP]
skip
[GOAL]
case f.h.f
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
x✝ : R
| fun x => ↑χ x * ↑ψ x * (↑χ x✝⁻¹ * ↑ψ (-x✝))
[PROOFSTEP]
ext
[GOAL]
case f.h.f.h
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
x✝¹ x✝ : R
| ↑χ x✝ * ↑ψ x✝ * (↑χ x✝¹⁻¹ * ↑ψ (-x✝¹))
[PROOFSTEP]
rw [mul_mul_mul_comm, ← map_mul, ← map_add_mul, ← sub_eq_add_neg]
  --  conv in _ * _ * (_ * _) => rw [mul_mul_mul_comm, ← map_mul, ← map_add_mul, ← sub_eq_add_neg]
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ ∑ x : R, ∑ x_1 : R, ↑χ (x_1 * x⁻¹) * ↑ψ (x_1 - x) = ↑(Fintype.card R)
[PROOFSTEP]
simp_rw [gaussSum_mul_aux hχ ψ]
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ ∑ x : R, ∑ x_1 : R, ↑χ x_1 * ↑ψ (x * (x_1 - 1)) = ↑(Fintype.card R)
[PROOFSTEP]
rw [Finset.sum_comm]
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ ∑ y : R, ∑ x : R, ↑χ y * ↑ψ (x * (y - 1)) = ↑(Fintype.card R)
[PROOFSTEP]
classical
  -- to get `[DecidableEq R]` for `sum_mulShift`
simp_rw [← Finset.mul_sum, sum_mulShift _ hψ, sub_eq_zero, apply_ite, Nat.cast_zero, mul_zero]
rw [Finset.sum_ite_eq' Finset.univ (1 : R)]
simp only [Finset.mem_univ, map_one, one_mul, if_true]
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ ∑ y : R, ∑ x : R, ↑χ y * ↑ψ (x * (y - 1)) = ↑(Fintype.card R)
[PROOFSTEP]
simp_rw [← Finset.mul_sum, sum_mulShift _ hψ, sub_eq_zero, apply_ite, Nat.cast_zero, mul_zero]
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ (∑ x : R, if x = 1 then ↑χ x * ↑(Fintype.card R) else 0) = ↑(Fintype.card R)
[PROOFSTEP]
rw [Finset.sum_ite_eq' Finset.univ (1 : R)]
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : MulChar.IsNontrivial χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ (if 1 ∈ Finset.univ then ↑χ 1 * ↑(Fintype.card R) else 0) = ↑(Fintype.card R)
[PROOFSTEP]
simp only [Finset.mem_univ, map_one, one_mul, if_true]
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : MulChar.IsNontrivial χ
hχ₂ : IsQuadratic χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ gaussSum χ ψ ^ 2 = ↑χ (-1) * ↑(Fintype.card R)
[PROOFSTEP]
rw [pow_two, ← gaussSum_mul_gaussSum_eq_card hχ₁ hψ, hχ₂.inv, mul_rotate']
[GOAL]
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : MulChar.IsNontrivial χ
hχ₂ : IsQuadratic χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ gaussSum χ ψ * gaussSum χ ψ = gaussSum χ ψ * (gaussSum χ ψ⁻¹ * ↑χ (-1))
[PROOFSTEP]
congr
[GOAL]
case e_a
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : MulChar.IsNontrivial χ
hχ₂ : IsQuadratic χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ gaussSum χ ψ = gaussSum χ ψ⁻¹ * ↑χ (-1)
[PROOFSTEP]
rw [mul_comm, ← gaussSum_mulShift _ _ (-1 : Rˣ), inv_mulShift]
[GOAL]
case e_a
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : MulChar.IsNontrivial χ
hχ₂ : IsQuadratic χ
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ ↑χ ↑(-1) * gaussSum χ (mulShift ψ ↑(-1)) = ↑χ (-1) * gaussSum χ (mulShift ψ (-1))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p)
[PROOFSTEP]
rw [← frobenius_def, gaussSum, gaussSum, map_sum]
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x : R, ↑(frobenius R' p) (↑χ x * ↑ψ x) = ∑ a : R, ↑(χ ^ p) a * ↑(ψ ^ p) a
[PROOFSTEP]
simp_rw [pow_apply' χ fp.1.pos, map_mul, frobenius_def]
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x : R, ↑χ x ^ p * ↑ψ x ^ p = ∑ x : R, ↑χ x ^ p * ↑(ψ ^ p) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p = ↑χ ↑p * gaussSum χ ψ
[PROOFSTEP]
rw [gaussSum_frob, pow_mulShift, hχ.pow_char p, ← gaussSum_mulShift χ ψ hp.unit, ← mul_assoc, hp.unit_spec, ← pow_two, ←
  pow_apply' _ (by norm_num : 0 < 2), hχ.sq_eq_one, ← hp.unit_spec, one_apply_coe, one_mul]
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
n : ℕ
hp : IsUnit ↑p
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p ^ n = ↑χ (↑p ^ n) * gaussSum χ ψ
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p ^ Nat.zero = ↑χ (↑p ^ Nat.zero) * gaussSum χ ψ
[PROOFSTEP]
rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]
[GOAL]
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = ↑χ (↑p ^ n) * gaussSum χ ψ
⊢ gaussSum χ ψ ^ p ^ Nat.succ n = ↑χ (↑p ^ Nat.succ n) * gaussSum χ ψ
[PROOFSTEP]
rw [pow_succ, mul_comm p, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, mul_comm (p : R), map_mul,
  ← pow_apply' χ fp.1.pos ((p : R) ^ n), hχ.pow_char p]
[GOAL]
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = ↑χ (-1) * ↑(Fintype.card R)
⊢ (↑χ (-1) * ↑(Fintype.card R)) ^ (p ^ n / 2) = ↑χ (↑p ^ n)
[PROOFSTEP]
have : gaussSum χ ψ ≠ 0 := by
  intro hf; rw [hf, zero_pow (by norm_num : 0 < 2), eq_comm, mul_eq_zero] at hg 
  exact
    not_isUnit_prime_of_dvd_card p
      ((CharP.cast_eq_zero_iff R' p _).mp <| hg.resolve_left (isUnit_one.neg.map χ).ne_zero) hp
[GOAL]
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = ↑χ (-1) * ↑(Fintype.card R)
⊢ gaussSum χ ψ ≠ 0
[PROOFSTEP]
intro hf
[GOAL]
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = ↑χ (-1) * ↑(Fintype.card R)
hf : gaussSum χ ψ = 0
⊢ False
[PROOFSTEP]
rw [hf, zero_pow (by norm_num : 0 < 2), eq_comm, mul_eq_zero] at hg 
[GOAL]
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : 0 ^ 2 = ↑χ (-1) * ↑(Fintype.card R)
hf : gaussSum χ ψ = 0
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : ↑χ (-1) = 0 ∨ ↑(Fintype.card R) = 0
hf : gaussSum χ ψ = 0
⊢ False
[PROOFSTEP]
exact
  not_isUnit_prime_of_dvd_card p ((CharP.cast_eq_zero_iff R' p _).mp <| hg.resolve_left (isUnit_one.neg.map χ).ne_zero)
    hp
[GOAL]
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = ↑χ (-1) * ↑(Fintype.card R)
this : gaussSum χ ψ ≠ 0
⊢ (↑χ (-1) * ↑(Fintype.card R)) ^ (p ^ n / 2) = ↑χ (↑p ^ n)
[PROOFSTEP]
rw [← hg]
[GOAL]
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = ↑χ (-1) * ↑(Fintype.card R)
this : gaussSum χ ψ ≠ 0
⊢ (gaussSum χ ψ ^ 2) ^ (p ^ n / 2) = ↑χ (↑p ^ n)
[PROOFSTEP]
apply mul_right_cancel₀ this
[GOAL]
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : IsQuadratic χ
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = ↑χ (-1) * ↑(Fintype.card R)
this : gaussSum χ ψ ≠ 0
⊢ (gaussSum χ ψ ^ 2) ^ (p ^ n / 2) * gaussSum χ ψ = ↑χ (↑p ^ n) * gaussSum χ ψ
[PROOFSTEP]
rw [← hχ.gaussSum_frob_iter p n hp ψ, ← pow_mul, mul_comm, ← pow_succ,
  Nat.two_mul_div_two_add_one_of_odd (fp.1.eq_two_or_odd'.resolve_left hp').pow]
[GOAL]
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
hχ₂ : IsQuadratic χ
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
⊢ (↑χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = ↑χ ↑(Fintype.card F')
[PROOFSTEP]
obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)
[GOAL]
case intro.intro
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
hχ₂ : IsQuadratic χ
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
⊢ (↑χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = ↑χ ↑(Fintype.card F')
[PROOFSTEP]
obtain ⟨n', hp', hc'⟩ := FiniteField.card F' (ringChar F')
[GOAL]
case intro.intro.intro.intro
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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'
⊢ (↑χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = ↑χ ↑(Fintype.card F')
[PROOFSTEP]
let ψ := primitiveCharFiniteField F F' hch₁
[GOAL]
case intro.intro.intro.intro
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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' := primitiveCharFiniteField F F' hch₁
⊢ (↑χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = ↑χ ↑(Fintype.card F')
[PROOFSTEP]
set FF' := CyclotomicField ψ.n F' with FF'_def
[GOAL]
case intro.intro.intro.intro
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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' := primitiveCharFiniteField F F' hch₁
FF' : Type u_2 := CyclotomicField (PrimitiveAddChar.n ψ) F'
FF'_def : FF' = CyclotomicField (PrimitiveAddChar.n ψ) F'
⊢ (↑χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = ↑χ ↑(Fintype.card F')
[PROOFSTEP]
have hchar := Algebra.ringChar_eq F' FF'
[GOAL]
case intro.intro.intro.intro
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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' := primitiveCharFiniteField F F' hch₁
FF' : Type u_2 := CyclotomicField (PrimitiveAddChar.n ψ) F'
FF'_def : FF' = CyclotomicField (PrimitiveAddChar.n ψ) F'
hchar : ringChar F' = ringChar FF'
⊢ (↑χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = ↑χ ↑(Fintype.card F')
[PROOFSTEP]
apply (algebraMap F' FF').injective
[GOAL]
case intro.intro.intro.intro.a
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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' := primitiveCharFiniteField F F' hch₁
FF' : Type u_2 := CyclotomicField (PrimitiveAddChar.n ψ) F'
FF'_def : FF' = CyclotomicField (PrimitiveAddChar.n ψ) F'
hchar : ringChar F' = ringChar FF'
⊢ ↑(algebraMap F' FF') ((↑χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2)) =
    ↑(algebraMap F' FF') (↑χ ↑(Fintype.card F'))
[PROOFSTEP]
rw [map_pow, map_mul, map_natCast, hc', hchar, Nat.cast_pow]
[GOAL]
case intro.intro.intro.intro.a
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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' := primitiveCharFiniteField F F' hch₁
FF' : Type u_2 := CyclotomicField (PrimitiveAddChar.n ψ) F'
FF'_def : FF' = CyclotomicField (PrimitiveAddChar.n ψ) F'
hchar : ringChar F' = ringChar FF'
⊢ (↑(algebraMap F' FF') (↑χ (-1)) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) =
    ↑(algebraMap F' FF') (↑χ (↑(ringChar FF') ^ ↑n'))
[PROOFSTEP]
simp only [← MulChar.ringHomComp_apply]
[GOAL]
case intro.intro.intro.intro.a
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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' := primitiveCharFiniteField F F' hch₁
FF' : Type u_2 := CyclotomicField (PrimitiveAddChar.n ψ) F'
FF'_def : FF' = CyclotomicField (PrimitiveAddChar.n ψ) F'
hchar : ringChar F' = ringChar FF'
⊢ (↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F')))
          (-1) *
        ↑(Fintype.card F)) ^
      (ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F') ^ ↑n' / 2) =
    ↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F')))
      (↑(ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F')) ^ ↑n')
[PROOFSTEP]
haveI := Fact.mk hp'
[GOAL]
case intro.intro.intro.intro.a
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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' := primitiveCharFiniteField F F' hch₁
FF' : Type u_2 := CyclotomicField (PrimitiveAddChar.n ψ) F'
FF'_def : FF' = CyclotomicField (PrimitiveAddChar.n ψ) F'
hchar : ringChar F' = ringChar FF'
this : Fact (Nat.Prime (ringChar F'))
⊢ (↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F')))
          (-1) *
        ↑(Fintype.card F)) ^
      (ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F') ^ ↑n' / 2) =
    ↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F')))
      (↑(ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F')) ^ ↑n')
[PROOFSTEP]
haveI := Fact.mk (hchar.subst hp')
[GOAL]
case intro.intro.intro.intro.a
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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' := primitiveCharFiniteField F F' hch₁
FF' : Type u_2 := CyclotomicField (PrimitiveAddChar.n ψ) F'
FF'_def : FF' = CyclotomicField (PrimitiveAddChar.n ψ) F'
hchar : ringChar F' = ringChar FF'
this✝ : Fact (Nat.Prime (ringChar F'))
this : Fact (Nat.Prime (ringChar FF'))
⊢ (↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F')))
          (-1) *
        ↑(Fintype.card F)) ^
      (ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F') ^ ↑n' / 2) =
    ↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F')))
      (↑(ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁)) F')) ^ ↑n')
[PROOFSTEP]
rw [Ne, ← Nat.prime_dvd_prime_iff_eq hp' hp, ← isUnit_iff_not_dvd_char, hchar] at hch₁ 
[GOAL]
case intro.intro.intro.intro.a
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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' := primitiveCharFiniteField F F' hch₁✝
FF' : Type u_2 := CyclotomicField (PrimitiveAddChar.n ψ) F'
hch₁ : IsUnit ↑(ringChar FF')
FF'_def : FF' = CyclotomicField (PrimitiveAddChar.n ψ) F'
hchar : ringChar F' = ringChar FF'
this✝ : Fact (Nat.Prime (ringChar F'))
this : Fact (Nat.Prime (ringChar FF'))
⊢ (↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')))
          (-1) *
        ↑(Fintype.card F)) ^
      (ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F') ^ ↑n' / 2) =
    ↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')))
      (↑(ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')) ^ ↑n')
[PROOFSTEP]
have :=
  Char.card_pow_char_pow (hχ₂.comp (algebraMap F' FF')) ψ.char (ringChar FF') n' hch₁ (hchar ▸ hch₂)
    (gaussSum_sq (hχ₁.comp <| RingHom.injective _) (hχ₂.comp _) ψ.prim)
[GOAL]
case intro.intro.intro.intro.a
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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' := primitiveCharFiniteField F F' hch₁✝
FF' : Type u_2 := CyclotomicField (PrimitiveAddChar.n ψ) F'
hch₁ : IsUnit ↑(ringChar FF')
FF'_def : FF' = CyclotomicField (PrimitiveAddChar.n ψ) F'
hchar : ringChar F' = ringChar FF'
this✝¹ : Fact (Nat.Prime (ringChar F'))
this✝ : Fact (Nat.Prime (ringChar FF'))
this :
  (↑(ringHomComp χ (algebraMap F' FF')) (-1) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) =
    ↑(ringHomComp χ (algebraMap F' FF')) (↑(ringChar FF') ^ ↑n')
⊢ (↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')))
          (-1) *
        ↑(Fintype.card F)) ^
      (ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F') ^ ↑n' / 2) =
    ↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')))
      (↑(ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')) ^ ↑n')
[PROOFSTEP]
simp_rw [FF'_def] at this 
[GOAL]
case intro.intro.intro.intro.a
R : Type u
inst✝⁷ : CommRing R
inst✝⁶ : Fintype R
R' : Type v
inst✝⁵ : CommRing R'
inst✝⁴ : IsDomain R'
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : MulChar.IsNontrivial χ
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' := primitiveCharFiniteField F F' hch₁✝
FF' : Type u_2 := CyclotomicField (PrimitiveAddChar.n ψ) F'
hch₁ : IsUnit ↑(ringChar FF')
FF'_def : FF' = CyclotomicField (PrimitiveAddChar.n ψ) F'
hchar : ringChar F' = ringChar FF'
this✝¹ : Fact (Nat.Prime (ringChar F'))
this✝ : Fact (Nat.Prime (ringChar FF'))
this :
  (↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')))
          (-1) *
        ↑(Fintype.card F)) ^
      (ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F') ^ ↑n' / 2) =
    ↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')))
      (↑(ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')) ^ ↑n')
⊢ (↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')))
          (-1) *
        ↑(Fintype.card F)) ^
      (ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F') ^ ↑n' / 2) =
    ↑(ringHomComp χ (algebraMap F' (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')))
      (↑(ringChar (CyclotomicField (PrimitiveAddChar.n (primitiveCharFiniteField F F' hch₁✝)) F')) ^ ↑n')
[PROOFSTEP]
exact this
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
have hp2 : ∀ n : ℕ, (2 ^ n : F) ≠ 0 := fun n => pow_ne_zero n (Ring.two_ne_zero hF)
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
obtain ⟨n, hp, hc⟩ :=
  FiniteField.card F
    (ringChar F)
      -- we work in `FF`, the eighth cyclotomic field extension of `F`
        -- Porting note: was
        -- let FF := (Polynomial.cyclotomic 8 F).SplittingField
        -- but we want to unify with `CyclotomicField` below.
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
let FF := CyclotomicField 8 F
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
haveI : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F) := Polynomial.IsSplittingField.splittingField _
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
haveI : FiniteDimensional F FF := Polynomial.IsSplittingField.finiteDimensional FF (Polynomial.cyclotomic 8 F)
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝ : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this : FiniteDimensional F FF
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
haveI : Fintype FF := FiniteDimensional.fintypeOfFintype F FF
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝¹ : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝ : FiniteDimensional F FF
this : Fintype FF
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
have hchar := Algebra.ringChar_eq F FF
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝¹ : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝ : FiniteDimensional F FF
this : Fintype FF
hchar : ringChar F = ringChar FF
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
have FFp := hchar.subst hp
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝¹ : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝ : FiniteDimensional F FF
this : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
haveI := Fact.mk FFp
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
have hFF := ne_of_eq_of_ne hchar.symm hF
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
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
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
⊢ IsUnit ↑(ringChar FF)
[PROOFSTEP]
rw [isUnit_iff_not_dvd_char, ringChar_zmod_n]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
⊢ ¬ringChar FF ∣ 8
[PROOFSTEP]
rw [Ne, ← Nat.prime_dvd_prime_iff_eq FFp Nat.prime_two] at hFF 
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ¬ringChar FF ∣ 2
⊢ ¬ringChar FF ∣ 8
[PROOFSTEP]
change ¬_ ∣ 2 ^ 3
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ¬ringChar FF ∣ 2
⊢ ¬ringChar FF ∣ 2 ^ 3
[PROOFSTEP]
exact mt FFp.dvd_of_dvd_pow hFF
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
let ψ₈ : PrimitiveAddChar (ZMod 8) F :=
  primitiveZModChar 8 F
    (by convert hp2 3 using 1; norm_cast)
      -- Porting note: unifying this is very slow, so only do it once.
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
⊢ ↑↑8 ≠ 0
[PROOFSTEP]
convert hp2 3 using 1
[GOAL]
case h.e'_2
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
⊢ ↑↑8 = 2 ^ 3
[PROOFSTEP]
norm_cast
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
let ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
let τ : FF := ψ₈char 1
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
have τ_spec : τ ^ 4 = -1 := by
  refine (sq_eq_one_iff.1 ?_).resolve_left ?_
  · rw [← pow_mul, ← map_nsmul_pow ψ₈char, AddChar.IsPrimitive.zmod_char_eq_one_iff 8 ψ₈.prim]
    decide
  · rw [← map_nsmul_pow ψ₈char, AddChar.IsPrimitive.zmod_char_eq_one_iff 8 ψ₈.prim]
    decide
      -- we consider `χ₈` as a multiplicative character `ℤ/8ℤ → FF`
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
⊢ τ ^ 4 = -1
[PROOFSTEP]
refine (sq_eq_one_iff.1 ?_).resolve_left ?_
[GOAL]
case refine_1
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
⊢ (τ ^ 4) ^ 2 = 1
[PROOFSTEP]
rw [← pow_mul, ← map_nsmul_pow ψ₈char, AddChar.IsPrimitive.zmod_char_eq_one_iff 8 ψ₈.prim]
[GOAL]
case refine_1
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
⊢ (4 * 2) • 1 = 0
[PROOFSTEP]
decide
[GOAL]
case refine_2
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
⊢ ¬τ ^ 4 = 1
[PROOFSTEP]
rw [← map_nsmul_pow ψ₈char, AddChar.IsPrimitive.zmod_char_eq_one_iff 8 ψ₈.prim]
[GOAL]
case refine_2
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
⊢ ¬4 • 1 = 0
[PROOFSTEP]
decide
  -- we consider `χ₈` as a multiplicative character `ℤ/8ℤ → FF`
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
let χ := χ₈.ringHomComp (Int.castRingHom FF)
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
have hχ : χ (-1) = 1 := Int.cast_one
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
have hq : IsQuadratic χ :=
  isQuadratic_χ₈.comp
    _
      -- we now show that the Gauss sum of `χ` and `ψ₈` has the relevant property
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
have hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * Fintype.card (ZMod 8) :=
  by
  have _ := congr_arg (· ^ 2) (Fin.sum_univ_eight fun x => (χ₈ x : FF) * τ ^ x.1)
  have h₁ : (fun i : Fin 8 => ↑(χ₈ i) * τ ^ i.val) = (fun a : ZMod 8 => χ a * ↑(ψ₈char a)) := by
    -- Porting note: original proof
          -- ext; congr; apply pow_oneext (x : Fin 8); rw [← map_nsmul_pow ψ₈char]; congr 2;
    rw [Nat.smul_one_eq_coe, Fin.cast_val_eq_self x]
  have h₂ :
    (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
      8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) :=
    by ring
  have h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = ↑8 := by rw [τ_spec]; norm_num
  have h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = ↑8 := by rw [← h₃, ← h₂]
  have h₅ :
    (↑(χ₈ 0) * τ ^ 0 + ↑(χ₈ 1) * τ ^ 1 + ↑(χ₈ 2) * τ ^ 2 + ↑(χ₈ 3) * τ ^ 3 + ↑(χ₈ 4) * τ ^ 4 + ↑(χ₈ 5) * τ ^ 5 +
            ↑(χ₈ 6) * τ ^ 6 +
          ↑(χ₈ 7) * τ ^ 7) ^
        2 =
      8 :=
    by
    -- Porting note: original proof
          --  simp [← h₄, χ₈_apply, Matrix.cons_val_zero, algebraMap.coe_zero, zero_mul,
          -- Matrix.cons_val_one, Matrix.head_cons, algebraMap.coe_one, Matrix.cons_vec_bit0_eq_alt0,
          -- Matrix.cons_vecAppend, Matrix.cons_vecAlt0, Matrix.cons_vec_bit1_eq_alt1,
          -- Matrix.cons_vecAlt1, Int.cast_neg]
    simp_rw [χ₈_apply]
    rw [← h₄]
    dsimp only
    congr
    · rw [Matrix.cons_val_zero]; simp
    · simp only [Matrix.vecCons, ne_eq, Nat.cast_ofNat, id_eq, eq_mpr_eq_cast, mul_eq_zero, zero_lt_two,
        pow_eq_zero_iff]
      left
      rw [← Int.cast_zero (R := FF)]
      exact congr_arg Int.cast rfl
    · simp only [Matrix.vecCons]
      rw [show (-1 : FF) = ↑(-1 : ℤ) by simp only [Int.cast_neg, Int.cast_one]]
      exact congr_arg Int.cast rfl
    · simp only [Matrix.vecCons, ne_eq, Nat.cast_ofNat, id_eq, eq_mpr_eq_cast, mul_eq_zero, zero_lt_two,
        pow_eq_zero_iff]
      left
      rw [← Int.cast_zero (R := FF)]
      exact congr_arg Int.cast rfl
    · simp only [Matrix.vecCons]
      rw [show (-1 : FF) = ↑(-1 : ℤ) by simp only [Int.cast_neg, Int.cast_one]]
      exact congr_arg Int.cast rfl
    · simp only [Matrix.vecCons, ne_eq, Nat.cast_ofNat, id_eq, eq_mpr_eq_cast, mul_eq_zero, zero_lt_two,
        pow_eq_zero_iff]
      left
      rw [← Int.cast_zero (R := FF)]
      exact congr_arg Int.cast rfl
  rw [gaussSum, hχ, one_mul, ZMod.card, Nat.cast_ofNat, ← h₅]
  simp_rw [← h₁]
  rw [Fin.sum_univ_eight]
  rfl
    -- this allows us to apply `card_pow_char_pow` to our situation
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
⊢ gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
[PROOFSTEP]
have _ := congr_arg (· ^ 2) (Fin.sum_univ_eight fun x => (χ₈ x : FF) * τ ^ x.1)
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
⊢ gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
[PROOFSTEP]
have h₁ : (fun i : Fin 8 => ↑(χ₈ i) * τ ^ i.val) = (fun a : ZMod 8 => χ a * ↑(ψ₈char a)) := by
  -- Porting note: original proof
        -- ext; congr; apply pow_oneext (x : Fin 8); rw [← map_nsmul_pow ψ₈char]; congr 2;
  rw [Nat.smul_one_eq_coe, Fin.cast_val_eq_self x]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
⊢ (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
[PROOFSTEP]
ext (x : Fin 8)
[GOAL]
case h
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
x : Fin 8
⊢ ↑(↑χ₈ x) * τ ^ ↑x = ↑χ x * ↑ψ₈char x
[PROOFSTEP]
rw [← map_nsmul_pow ψ₈char]
[GOAL]
case h
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
x : Fin 8
⊢ ↑(↑χ₈ x) * ↑ψ₈char (↑x • 1) = ↑χ x * ↑ψ₈char x
[PROOFSTEP]
congr 2
[GOAL]
case h.e_a.e_x
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
x : Fin 8
⊢ ↑x • 1 = x
[PROOFSTEP]
rw [Nat.smul_one_eq_coe, Fin.cast_val_eq_self x]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
⊢ gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
[PROOFSTEP]
have h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) :=
  by ring
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
⊢ (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
[PROOFSTEP]
ring
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
⊢ gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
[PROOFSTEP]
have h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = ↑8 := by rw [τ_spec]; norm_num
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
⊢ 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
[PROOFSTEP]
rw [τ_spec]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
⊢ 8 + (-1 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * -1 + τ ^ 2 - 8) = 8
[PROOFSTEP]
norm_num
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
⊢ gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
[PROOFSTEP]
have h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = ↑8 := by rw [← h₃, ← h₂]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
⊢ (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
[PROOFSTEP]
rw [← h₃, ← h₂]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
[PROOFSTEP]
have h₅ :
  (↑(χ₈ 0) * τ ^ 0 + ↑(χ₈ 1) * τ ^ 1 + ↑(χ₈ 2) * τ ^ 2 + ↑(χ₈ 3) * τ ^ 3 + ↑(χ₈ 4) * τ ^ 4 + ↑(χ₈ 5) * τ ^ 5 +
          ↑(χ₈ 6) * τ ^ 6 +
        ↑(χ₈ 7) * τ ^ 7) ^
      2 =
    8 :=
  by
  -- Porting note: original proof
        --  simp [← h₄, χ₈_apply, Matrix.cons_val_zero, algebraMap.coe_zero, zero_mul,
        -- Matrix.cons_val_one, Matrix.head_cons, algebraMap.coe_one, Matrix.cons_vec_bit0_eq_alt0,
        -- Matrix.cons_vecAppend, Matrix.cons_vecAlt0, Matrix.cons_vec_bit1_eq_alt1,
        -- Matrix.cons_vecAlt1, Int.cast_neg]
  simp_rw [χ₈_apply]
  rw [← h₄]
  dsimp only
  congr
  · rw [Matrix.cons_val_zero]; simp
  · simp only [Matrix.vecCons, ne_eq, Nat.cast_ofNat, id_eq, eq_mpr_eq_cast, mul_eq_zero, zero_lt_two, pow_eq_zero_iff]
    left
    rw [← Int.cast_zero (R := FF)]
    exact congr_arg Int.cast rfl
  · simp only [Matrix.vecCons]
    rw [show (-1 : FF) = ↑(-1 : ℤ) by simp only [Int.cast_neg, Int.cast_one]]
    exact congr_arg Int.cast rfl
  · simp only [Matrix.vecCons, ne_eq, Nat.cast_ofNat, id_eq, eq_mpr_eq_cast, mul_eq_zero, zero_lt_two, pow_eq_zero_iff]
    left
    rw [← Int.cast_zero (R := FF)]
    exact congr_arg Int.cast rfl
  · simp only [Matrix.vecCons]
    rw [show (-1 : FF) = ↑(-1 : ℤ) by simp only [Int.cast_neg, Int.cast_one]]
    exact congr_arg Int.cast rfl
  · simp only [Matrix.vecCons, ne_eq, Nat.cast_ofNat, id_eq, eq_mpr_eq_cast, mul_eq_zero, zero_lt_two, pow_eq_zero_iff]
    left
    rw [← Int.cast_zero (R := FF)]
    exact congr_arg Int.cast rfl
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ (↑(↑χ₈ 0) * τ ^ 0 + ↑(↑χ₈ 1) * τ ^ 1 + ↑(↑χ₈ 2) * τ ^ 2 + ↑(↑χ₈ 3) * τ ^ 3 + ↑(↑χ₈ 4) * τ ^ 4 + ↑(↑χ₈ 5) * τ ^ 5 +
          ↑(↑χ₈ 6) * τ ^ 6 +
        ↑(↑χ₈ 7) * τ ^ 7) ^
      2 =
    8
[PROOFSTEP]
simp_rw [χ₈_apply]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ (↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 0) *
                      ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 0 +
                    ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1) *
                      ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 1 +
                  ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 2) *
                    ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 2 +
                ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 3) *
                  ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 3 +
              ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 4) *
                ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 4 +
            ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 5) *
              ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 5 +
          ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 6) *
            ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 6 +
        ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 7) *
          ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 7) ^
      2 =
    8
[PROOFSTEP]
rw [← h₄]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ (↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 0) *
                      ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 0 +
                    ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1) *
                      ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 1 +
                  ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 2) *
                    ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 2 +
                ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 3) *
                  ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 3 +
              ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 4) *
                ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 4 +
            ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 5) *
              ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 5 +
          ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 6) *
            ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 6 +
        ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 7) *
          ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 7) ^
      2 =
    (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2
[PROOFSTEP]
dsimp only
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ (↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 0) *
                      ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 0 +
                    ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1) *
                      ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 1 +
                  ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 2) *
                    ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 2 +
                ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 3) *
                  ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 3 +
              ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 4) *
                ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 4 +
            ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 5) *
              ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 5 +
          ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 6) *
            ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 6 +
        ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 7) *
          ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 7) ^
      2 =
    (0 + 1 * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 1 + 0 +
                -1 * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 3 +
              0 +
            -1 * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 5 +
          0 +
        1 * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 7) ^
      2
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a.e_a.e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 0) *
      ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 0 =
    0
[PROOFSTEP]
rw [Matrix.cons_val_zero]
[GOAL]
case e_a.e_a.e_a.e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑0 * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 0 = 0
[PROOFSTEP]
simp
[GOAL]
case e_a.e_a.e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 2) *
      ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 2 =
    0
[PROOFSTEP]
simp only [Matrix.vecCons, ne_eq, Nat.cast_ofNat, id_eq, eq_mpr_eq_cast, mul_eq_zero, zero_lt_two, pow_eq_zero_iff]
[GOAL]
case e_a.e_a.e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 2) =
      0 ∨
    ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ¬↑↑8 = 0))) 1 = 0
[PROOFSTEP]
left
[GOAL]
case e_a.e_a.e_a.e_a.e_a.e_a.e_a.h
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 2) =
    0
[PROOFSTEP]
rw [← Int.cast_zero (R := FF)]
[GOAL]
case e_a.e_a.e_a.e_a.e_a.e_a.e_a.h
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 2) =
    ↑0
[PROOFSTEP]
exact congr_arg Int.cast rfl
[GOAL]
case e_a.e_a.e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 3) = -1
[PROOFSTEP]
simp only [Matrix.vecCons]
[GOAL]
case e_a.e_a.e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 3) =
    -1
[PROOFSTEP]
rw [show (-1 : FF) = ↑(-1 : ℤ) by simp only [Int.cast_neg, Int.cast_one]]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ -1 = ↑(-1)
[PROOFSTEP]
simp only [Int.cast_neg, Int.cast_one]
[GOAL]
case e_a.e_a.e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 3) =
    ↑(-1)
[PROOFSTEP]
exact congr_arg Int.cast rfl
[GOAL]
case e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 4) *
      ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 4 =
    0
[PROOFSTEP]
simp only [Matrix.vecCons, ne_eq, Nat.cast_ofNat, id_eq, eq_mpr_eq_cast, mul_eq_zero, zero_lt_two, pow_eq_zero_iff]
[GOAL]
case e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 4) =
      0 ∨
    ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ¬↑↑8 = 0))) 1 = 0
[PROOFSTEP]
left
[GOAL]
case e_a.e_a.e_a.e_a.e_a.h
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 4) =
    0
[PROOFSTEP]
rw [← Int.cast_zero (R := FF)]
[GOAL]
case e_a.e_a.e_a.e_a.e_a.h
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 4) =
    ↑0
[PROOFSTEP]
exact congr_arg Int.cast rfl
[GOAL]
case e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 5) = -1
[PROOFSTEP]
simp only [Matrix.vecCons]
[GOAL]
case e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 5) =
    -1
[PROOFSTEP]
rw [show (-1 : FF) = ↑(-1 : ℤ) by simp only [Int.cast_neg, Int.cast_one]]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ -1 = ↑(-1)
[PROOFSTEP]
simp only [Int.cast_neg, Int.cast_one]
[GOAL]
case e_a.e_a.e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 5) =
    ↑(-1)
[PROOFSTEP]
exact congr_arg Int.cast rfl
[GOAL]
case e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 6) *
      ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 6 =
    0
[PROOFSTEP]
simp only [Matrix.vecCons, ne_eq, Nat.cast_ofNat, id_eq, eq_mpr_eq_cast, mul_eq_zero, zero_lt_two, pow_eq_zero_iff]
[GOAL]
case e_a.e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 6) =
      0 ∨
    ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ¬↑↑8 = 0))) 1 = 0
[PROOFSTEP]
left
[GOAL]
case e_a.e_a.e_a.h
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 6) =
    0
[PROOFSTEP]
rw [← Int.cast_zero (R := FF)]
[GOAL]
case e_a.e_a.e_a.h
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
⊢ ↑(Fin.cons 0 (Fin.cons 1 (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons (-1) (Fin.cons 0 (Fin.cons 1 ![]))))))) 6) =
    ↑0
[PROOFSTEP]
exact congr_arg Int.cast rfl
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
h₅ :
  (↑(↑χ₈ 0) * τ ^ 0 + ↑(↑χ₈ 1) * τ ^ 1 + ↑(↑χ₈ 2) * τ ^ 2 + ↑(↑χ₈ 3) * τ ^ 3 + ↑(↑χ₈ 4) * τ ^ 4 + ↑(↑χ₈ 5) * τ ^ 5 +
          ↑(↑χ₈ 6) * τ ^ 6 +
        ↑(↑χ₈ 7) * τ ^ 7) ^
      2 =
    8
⊢ gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
[PROOFSTEP]
rw [gaussSum, hχ, one_mul, ZMod.card, Nat.cast_ofNat, ← h₅]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
h₅ :
  (↑(↑χ₈ 0) * τ ^ 0 + ↑(↑χ₈ 1) * τ ^ 1 + ↑(↑χ₈ 2) * τ ^ 2 + ↑(↑χ₈ 3) * τ ^ 3 + ↑(↑χ₈ 4) * τ ^ 4 + ↑(↑χ₈ 5) * τ ^ 5 +
          ↑(↑χ₈ 6) * τ ^ 6 +
        ↑(↑χ₈ 7) * τ ^ 7) ^
      2 =
    8
⊢ (∑ a : ZMod 8, ↑χ a * ↑ψ₈char a) ^ 2 =
    (↑(↑χ₈ 0) * τ ^ 0 + ↑(↑χ₈ 1) * τ ^ 1 + ↑(↑χ₈ 2) * τ ^ 2 + ↑(↑χ₈ 3) * τ ^ 3 + ↑(↑χ₈ 4) * τ ^ 4 + ↑(↑χ₈ 5) * τ ^ 5 +
          ↑(↑χ₈ 6) * τ ^ 6 +
        ↑(↑χ₈ 7) * τ ^ 7) ^
      2
[PROOFSTEP]
simp_rw [← h₁]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
h₅ :
  (↑(↑χ₈ 0) * τ ^ 0 + ↑(↑χ₈ 1) * τ ^ 1 + ↑(↑χ₈ 2) * τ ^ 2 + ↑(↑χ₈ 3) * τ ^ 3 + ↑(↑χ₈ 4) * τ ^ 4 + ↑(↑χ₈ 5) * τ ^ 5 +
          ↑(↑χ₈ 6) * τ ^ 6 +
        ↑(↑χ₈ 7) * τ ^ 7) ^
      2 =
    8
⊢ (∑ i : ZMod 8, ↑(↑χ₈ i) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ ↑i) ^ 2 =
    (↑(↑χ₈ 0) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 0 +
                    ↑(↑χ₈ 1) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 1 +
                  ↑(↑χ₈ 2) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 2 +
                ↑(↑χ₈ 3) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 3 +
              ↑(↑χ₈ 4) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 4 +
            ↑(↑χ₈ 5) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 5 +
          ↑(↑χ₈ 6) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 6 +
        ↑(↑χ₈ 7) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 7) ^
      2
[PROOFSTEP]
rw [Fin.sum_univ_eight]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
x✝ :
  (fun x => x ^ 2) (∑ i : Fin 8, ↑(↑χ₈ i) * τ ^ ↑i) =
    (fun x => x ^ 2)
      (↑(↑χ₈ 0) * τ ^ ↑0 + ↑(↑χ₈ 1) * τ ^ ↑1 + ↑(↑χ₈ 2) * τ ^ ↑2 + ↑(↑χ₈ 3) * τ ^ ↑3 + ↑(↑χ₈ 4) * τ ^ ↑4 +
            ↑(↑χ₈ 5) * τ ^ ↑5 +
          ↑(↑χ₈ 6) * τ ^ ↑6 +
        ↑(↑χ₈ 7) * τ ^ ↑7)
h₁ : (fun i => ↑(↑χ₈ i) * τ ^ ↑i) = fun a => ↑χ a * ↑ψ₈char a
h₂ :
  (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 =
    8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8)
h₃ : 8 + (τ ^ 4 + 1) * (τ ^ 10 - 2 * τ ^ 8 - 2 * τ ^ 6 + 6 * τ ^ 4 + τ ^ 2 - 8) = 8
h₄ : (0 + 1 * τ ^ 1 + 0 + -1 * τ ^ 3 + 0 + -1 * τ ^ 5 + 0 + 1 * τ ^ 7) ^ 2 = 8
h₅ :
  (↑(↑χ₈ 0) * τ ^ 0 + ↑(↑χ₈ 1) * τ ^ 1 + ↑(↑χ₈ 2) * τ ^ 2 + ↑(↑χ₈ 3) * τ ^ 3 + ↑(↑χ₈ 4) * τ ^ 4 + ↑(↑χ₈ 5) * τ ^ 5 +
          ↑(↑χ₈ 6) * τ ^ 6 +
        ↑(↑χ₈ 7) * τ ^ 7) ^
      2 =
    8
⊢ (↑(↑χ₈ 0) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ ↑0 +
                    ↑(↑χ₈ 1) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ ↑1 +
                  ↑(↑χ₈ 2) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ ↑2 +
                ↑(↑χ₈ 3) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ ↑3 +
              ↑(↑χ₈ 4) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ ↑4 +
            ↑(↑χ₈ 5) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ ↑5 +
          ↑(↑χ₈ 6) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ ↑6 +
        ↑(↑χ₈ 7) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ ↑7) ^
      2 =
    (↑(↑χ₈ 0) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 0 +
                    ↑(↑χ₈ 1) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 1 +
                  ↑(↑χ₈ 2) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 2 +
                ↑(↑χ₈ 3) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 3 +
              ↑(↑χ₈ 4) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 4 +
            ↑(↑χ₈ 5) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 5 +
          ↑(↑χ₈ 6) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 6 +
        ↑(↑χ₈ 7) * ↑(PrimitiveAddChar.char (primitiveZModChar 8 F (_ : ↑↑8 ≠ 0))) 1 ^ 7) ^
      2
[PROOFSTEP]
rfl
  -- this allows us to apply `card_pow_char_pow` to our situation
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
hg : gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
have h := Char.card_pow_char_pow (R := ZMod 8) hq ψ₈char (ringChar FF) n hu hFF hg
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
hg : gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
h : (↑χ (-1) * ↑(Fintype.card (ZMod 8))) ^ (ringChar FF ^ ↑n / 2) = ↑χ (↑(ringChar FF) ^ ↑n)
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
rw [ZMod.card, ← hchar, hχ, one_mul, ← hc, ← Nat.cast_pow (ringChar F), ← hc] at h 
[GOAL]
case intro.intro
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
hg : gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = ↑χ ↑(Fintype.card F)
⊢ 2 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
convert_to (8 : F) ^ (Fintype.card F / 2) = _
[GOAL]
case h.e'_2
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
hg : gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = ↑χ ↑(Fintype.card F)
⊢ 2 ^ (Fintype.card F / 2) = 8 ^ (Fintype.card F / 2)
[PROOFSTEP]
rw [(by norm_num : (8 : F) = 2 ^ 2 * 2), mul_pow, (FiniteField.isSquare_iff hF <| hp2 2).mp ⟨2, pow_two 2⟩, one_mul]
[GOAL]
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
hg : gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = ↑χ ↑(Fintype.card F)
⊢ 8 = 2 ^ 2 * 2
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro.convert_2
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
hg : gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = ↑χ ↑(Fintype.card F)
⊢ 8 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
apply (algebraMap F FF).injective
[GOAL]
case intro.intro.convert_2.a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
hg : gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = ↑χ ↑(Fintype.card F)
⊢ ↑(algebraMap F FF) (8 ^ (Fintype.card F / 2)) = ↑(algebraMap F FF) ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
simp only [map_pow, map_ofNat, map_intCast]
[GOAL]
case intro.intro.convert_2.a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
hg : gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = ↑χ ↑(Fintype.card F)
⊢ 8 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
simp only [Nat.cast_ofNat, ringHomComp_apply, eq_intCast] at h 
[GOAL]
case intro.intro.convert_2.a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
this✝² : Polynomial.IsSplittingField F FF (Polynomial.cyclotomic 8 F)
this✝¹ : FiniteDimensional F FF
this✝ : Fintype FF
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod 8) F := primitiveZModChar 8 F (_ : ↑↑8 ≠ 0)
ψ₈char : AddChar (ZMod 8) FF := PrimitiveAddChar.char ψ₈
τ : FF := ↑ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ringHomComp χ₈ (Int.castRingHom FF)
hχ : ↑χ (-1) = 1
hq : IsQuadratic χ
hg : gaussSum χ ψ₈char ^ 2 = ↑χ (-1) * ↑(Fintype.card (ZMod 8))
h : 8 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
⊢ 8 ^ (Fintype.card F / 2) = ↑(↑χ₈ ↑(Fintype.card F))
[PROOFSTEP]
exact h
