[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
classical
by_cases hF : ringChar F = 2
focus
  have h := FiniteField.even_card_of_char_two hF
  simp only [FiniteField.isSquare_of_char_two hF, true_iff_iff]
rotate_left
focus
  have h := FiniteField.odd_card_of_char_ne_two hF
  rw [← quadraticChar_one_iff_isSquare (Ring.two_ne_zero hF), quadraticChar_two hF, χ₈_nat_eq_if_mod_eight]
  simp only [h, Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false,
    Classical.not_not]
all_goals
  rw [← Nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h
  have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8)
  revert h₁ h
  generalize Fintype.card F % 8 = n
  intros;
  interval_cases n <;>
    simp_all
      -- Porting note: was `decide!`
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
by_cases hF : ringChar F = 2
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
focus
  have h := FiniteField.even_card_of_char_two hF
  simp only [FiniteField.isSquare_of_char_two hF, true_iff_iff]
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
have h := FiniteField.even_card_of_char_two hF
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
simp only [FiniteField.isSquare_of_char_two hF, true_iff_iff]
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
rotate_left
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
focus
  have h := FiniteField.odd_card_of_char_ne_two hF
  rw [← quadraticChar_one_iff_isSquare (Ring.two_ne_zero hF), quadraticChar_two hF, χ₈_nat_eq_if_mod_eight]
  simp only [h, Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false,
    Classical.not_not]
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
have h := FiniteField.odd_card_of_char_ne_two hF
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
rw [← quadraticChar_one_iff_isSquare (Ring.two_ne_zero hF), quadraticChar_two hF, χ₈_nat_eq_if_mod_eight]
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
simp only [h, Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false,
  Classical.not_not]
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 ↔ ¬Fintype.card F % 8 = 3 ∧ ¬Fintype.card F % 8 = 5
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
all_goals
  rw [← Nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h
  have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8)
  revert h₁ h
  generalize Fintype.card F % 8 = n
  intros;
  interval_cases n <;>
    simp_all
      -- Porting note: was `decide!`
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 ↔ ¬Fintype.card F % 8 = 3 ∧ ¬Fintype.card F % 8 = 5
[PROOFSTEP]
rw [← Nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ 2 ∣ 8
[PROOFSTEP]
norm_num
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 8 % 2 = 1
⊢ Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 ↔ ¬Fintype.card F % 8 = 3 ∧ ¬Fintype.card F % 8 = 5
[PROOFSTEP]
have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8)
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 8 % 2 = 1
⊢ 0 < 8
[PROOFSTEP]
decide
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 8 % 2 = 1
h₁ : Fintype.card F % 8 < 8
⊢ Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 ↔ ¬Fintype.card F % 8 = 3 ∧ ¬Fintype.card F % 8 = 5
[PROOFSTEP]
revert h₁ h
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ Fintype.card F % 8 % 2 = 1 →
    Fintype.card F % 8 < 8 →
      (Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 ↔ ¬Fintype.card F % 8 = 3 ∧ ¬Fintype.card F % 8 = 5)
[PROOFSTEP]
generalize Fintype.card F % 8 = n
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
⊢ n % 2 = 1 → n < 8 → (n = 1 ∨ n = 7 ↔ ¬n = 3 ∧ ¬n = 5)
[PROOFSTEP]
intros
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : n % 2 = 1
h₁✝ : n < 8
⊢ n = 1 ∨ n = 7 ↔ ¬n = 3 ∧ ¬n = 5
[PROOFSTEP]
interval_cases n
[GOAL]
case neg.«0»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 0 % 2 = 1
h₁✝ : 0 < 8
⊢ 0 = 1 ∨ 0 = 7 ↔ ¬0 = 3 ∧ ¬0 = 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«1»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 1 % 2 = 1
h₁✝ : 1 < 8
⊢ 1 = 1 ∨ 1 = 7 ↔ ¬1 = 3 ∧ ¬1 = 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«2»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 2 % 2 = 1
h₁✝ : 2 < 8
⊢ 2 = 1 ∨ 2 = 7 ↔ ¬2 = 3 ∧ ¬2 = 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«3»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 3 % 2 = 1
h₁✝ : 3 < 8
⊢ 3 = 1 ∨ 3 = 7 ↔ ¬3 = 3 ∧ ¬3 = 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«4»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 4 % 2 = 1
h₁✝ : 4 < 8
⊢ 4 = 1 ∨ 4 = 7 ↔ ¬4 = 3 ∧ ¬4 = 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«5»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 5 % 2 = 1
h₁✝ : 5 < 8
⊢ 5 = 1 ∨ 5 = 7 ↔ ¬5 = 3 ∧ ¬5 = 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«6»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 6 % 2 = 1
h₁✝ : 6 < 8
⊢ 6 = 1 ∨ 6 = 7 ↔ ¬6 = 3 ∧ ¬6 = 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«7»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 7 % 2 = 1
h₁✝ : 7 < 8
⊢ 7 = 1 ∨ 7 = 7 ↔ ¬7 = 3 ∧ ¬7 = 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
rw [← Nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ 2 ∣ 8
[PROOFSTEP]
norm_num
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 8 % 2 = 0
⊢ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8)
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 8 % 2 = 0
⊢ 0 < 8
[PROOFSTEP]
decide
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 8 % 2 = 0
h₁ : Fintype.card F % 8 < 8
⊢ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
revert h₁ h
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ Fintype.card F % 8 % 2 = 0 → Fintype.card F % 8 < 8 → Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
[PROOFSTEP]
generalize Fintype.card F % 8 = n
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
⊢ n % 2 = 0 → n < 8 → n ≠ 3 ∧ n ≠ 5
[PROOFSTEP]
intros
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : n % 2 = 0
h₁✝ : n < 8
⊢ n ≠ 3 ∧ n ≠ 5
[PROOFSTEP]
interval_cases n
[GOAL]
case pos.«0»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 0 % 2 = 0
h₁✝ : 0 < 8
⊢ 0 ≠ 3 ∧ 0 ≠ 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«1»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 1 % 2 = 0
h₁✝ : 1 < 8
⊢ 1 ≠ 3 ∧ 1 ≠ 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«2»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 2 % 2 = 0
h₁✝ : 2 < 8
⊢ 2 ≠ 3 ∧ 2 ≠ 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«3»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 3 % 2 = 0
h₁✝ : 3 < 8
⊢ 3 ≠ 3 ∧ 3 ≠ 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«4»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 4 % 2 = 0
h₁✝ : 4 < 8
⊢ 4 ≠ 3 ∧ 4 ≠ 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«5»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 5 % 2 = 0
h₁✝ : 5 < 8
⊢ 5 ≠ 3 ∧ 5 ≠ 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«6»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 6 % 2 = 0
h₁✝ : 6 < 8
⊢ 6 ≠ 3 ∧ 6 ≠ 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«7»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 7 % 2 = 0
h₁✝ : 7 < 8
⊢ 7 ≠ 3 ∧ 7 ≠ 5
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ ↑(quadraticChar F) (-2) = ↑χ₈' ↑(Fintype.card F)
[PROOFSTEP]
rw [(by norm_num : (-2 : F) = -1 * 2), map_mul, χ₈'_eq_χ₄_mul_χ₈, quadraticChar_neg_one hF, quadraticChar_two hF,
  @cast_nat_cast _ (ZMod 4) _ _ _ (by norm_num : 4 ∣ 8)]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ -2 = -1 * 2
[PROOFSTEP]
norm_num
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ 4 ∣ 8
[PROOFSTEP]
norm_num
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
classical
by_cases hF : ringChar F = 2
focus
  have h := FiniteField.even_card_of_char_two hF
  simp only [FiniteField.isSquare_of_char_two hF, true_iff_iff]
rotate_left
focus
  have h := FiniteField.odd_card_of_char_ne_two hF
  rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (Ring.two_ne_zero hF)), quadraticChar_neg_two hF,
    χ₈'_nat_eq_if_mod_eight]
  simp only [h, Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false,
    Classical.not_not]
all_goals
  rw [← Nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h
  have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8)
  revert h₁ h
  generalize Fintype.card F % 8 = n
  intros;
  interval_cases n <;>
    simp_all
      -- Porting note: was `decide!`
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
by_cases hF : ringChar F = 2
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
focus
  have h := FiniteField.even_card_of_char_two hF
  simp only [FiniteField.isSquare_of_char_two hF, true_iff_iff]
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
have h := FiniteField.even_card_of_char_two hF
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
simp only [FiniteField.isSquare_of_char_two hF, true_iff_iff]
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
rotate_left
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
focus
  have h := FiniteField.odd_card_of_char_ne_two hF
  rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (Ring.two_ne_zero hF)), quadraticChar_neg_two hF,
    χ₈'_nat_eq_if_mod_eight]
  simp only [h, Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false,
    Classical.not_not]
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
have h := FiniteField.odd_card_of_char_ne_two hF
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (Ring.two_ne_zero hF)), quadraticChar_neg_two hF,
  χ₈'_nat_eq_if_mod_eight]
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 3 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
simp only [h, Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false,
  Classical.not_not]
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 3 ↔ ¬Fintype.card F % 8 = 5 ∧ ¬Fintype.card F % 8 = 7
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
all_goals
  rw [← Nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h
  have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8)
  revert h₁ h
  generalize Fintype.card F % 8 = n
  intros;
  interval_cases n <;>
    simp_all
      -- Porting note: was `decide!`
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 3 ↔ ¬Fintype.card F % 8 = 5 ∧ ¬Fintype.card F % 8 = 7
[PROOFSTEP]
rw [← Nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ 2 ∣ 8
[PROOFSTEP]
norm_num
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 8 % 2 = 1
⊢ Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 3 ↔ ¬Fintype.card F % 8 = 5 ∧ ¬Fintype.card F % 8 = 7
[PROOFSTEP]
have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8)
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 8 % 2 = 1
⊢ 0 < 8
[PROOFSTEP]
decide
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 8 % 2 = 1
h₁ : Fintype.card F % 8 < 8
⊢ Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 3 ↔ ¬Fintype.card F % 8 = 5 ∧ ¬Fintype.card F % 8 = 7
[PROOFSTEP]
revert h₁ h
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ Fintype.card F % 8 % 2 = 1 →
    Fintype.card F % 8 < 8 →
      (Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 3 ↔ ¬Fintype.card F % 8 = 5 ∧ ¬Fintype.card F % 8 = 7)
[PROOFSTEP]
generalize Fintype.card F % 8 = n
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
⊢ n % 2 = 1 → n < 8 → (n = 1 ∨ n = 3 ↔ ¬n = 5 ∧ ¬n = 7)
[PROOFSTEP]
intros
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : n % 2 = 1
h₁✝ : n < 8
⊢ n = 1 ∨ n = 3 ↔ ¬n = 5 ∧ ¬n = 7
[PROOFSTEP]
interval_cases n
[GOAL]
case neg.«0»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 0 % 2 = 1
h₁✝ : 0 < 8
⊢ 0 = 1 ∨ 0 = 3 ↔ ¬0 = 5 ∧ ¬0 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«1»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 1 % 2 = 1
h₁✝ : 1 < 8
⊢ 1 = 1 ∨ 1 = 3 ↔ ¬1 = 5 ∧ ¬1 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«2»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 2 % 2 = 1
h₁✝ : 2 < 8
⊢ 2 = 1 ∨ 2 = 3 ↔ ¬2 = 5 ∧ ¬2 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«3»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 3 % 2 = 1
h₁✝ : 3 < 8
⊢ 3 = 1 ∨ 3 = 3 ↔ ¬3 = 5 ∧ ¬3 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«4»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 4 % 2 = 1
h₁✝ : 4 < 8
⊢ 4 = 1 ∨ 4 = 3 ↔ ¬4 = 5 ∧ ¬4 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«5»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 5 % 2 = 1
h₁✝ : 5 < 8
⊢ 5 = 1 ∨ 5 = 3 ↔ ¬5 = 5 ∧ ¬5 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«6»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 6 % 2 = 1
h₁✝ : 6 < 8
⊢ 6 = 1 ∨ 6 = 3 ↔ ¬6 = 5 ∧ ¬6 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case neg.«7»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
n : ℕ
h✝ : 7 % 2 = 1
h₁✝ : 7 < 8
⊢ 7 = 1 ∨ 7 = 3 ↔ ¬7 = 5 ∧ ¬7 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
rw [← Nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ 2 ∣ 8
[PROOFSTEP]
norm_num
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 8 % 2 = 0
⊢ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8)
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 8 % 2 = 0
⊢ 0 < 8
[PROOFSTEP]
decide
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 8 % 2 = 0
h₁ : Fintype.card F % 8 < 8
⊢ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
revert h₁ h
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ Fintype.card F % 8 % 2 = 0 → Fintype.card F % 8 < 8 → Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
[PROOFSTEP]
generalize Fintype.card F % 8 = n
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
⊢ n % 2 = 0 → n < 8 → n ≠ 5 ∧ n ≠ 7
[PROOFSTEP]
intros
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : n % 2 = 0
h₁✝ : n < 8
⊢ n ≠ 5 ∧ n ≠ 7
[PROOFSTEP]
interval_cases n
[GOAL]
case pos.«0»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 0 % 2 = 0
h₁✝ : 0 < 8
⊢ 0 ≠ 5 ∧ 0 ≠ 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«1»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 1 % 2 = 0
h₁✝ : 1 < 8
⊢ 1 ≠ 5 ∧ 1 ≠ 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«2»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 2 % 2 = 0
h₁✝ : 2 < 8
⊢ 2 ≠ 5 ∧ 2 ≠ 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«3»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 3 % 2 = 0
h₁✝ : 3 < 8
⊢ 3 ≠ 5 ∧ 3 ≠ 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«4»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 4 % 2 = 0
h₁✝ : 4 < 8
⊢ 4 ≠ 5 ∧ 4 ≠ 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«5»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 5 % 2 = 0
h₁✝ : 5 < 8
⊢ 5 ≠ 5 ∧ 5 ≠ 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«6»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 6 % 2 = 0
h₁✝ : 6 < 8
⊢ 6 ≠ 5 ∧ 6 ≠ 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case pos.«7»
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
n : ℕ
h✝ : 7 % 2 = 0
h₁✝ : 7 < 8
⊢ 7 ≠ 5 ∧ 7 ≠ 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
⊢ ↑(quadraticChar F) ↑(Fintype.card F') = ↑(quadraticChar F') (↑(↑(quadraticChar F) (-1)) * ↑(Fintype.card F))
[PROOFSTEP]
let χ := (quadraticChar F).ringHomComp (algebraMap ℤ F')
[GOAL]
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
⊢ ↑(quadraticChar F) ↑(Fintype.card F') = ↑(quadraticChar F') (↑(↑(quadraticChar F) (-1)) * ↑(Fintype.card F))
[PROOFSTEP]
have hχ₁ : χ.IsNontrivial := by
  obtain ⟨a, ha⟩ := quadraticChar_exists_neg_one hF
  have hu : IsUnit a := by
    contrapose ha
    exact ne_of_eq_of_ne (map_nonunit (quadraticChar F) ha) (mt zero_eq_neg.mp one_ne_zero)
  use hu.unit
  simp only [IsUnit.unit_spec, ringHomComp_apply, eq_intCast, Ne.def, ha]
  rw [Int.cast_neg, Int.cast_one]
  exact Ring.neg_one_ne_one_of_char_ne_two hF'
[GOAL]
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
⊢ IsNontrivial χ
[PROOFSTEP]
obtain ⟨a, ha⟩ := quadraticChar_exists_neg_one hF
[GOAL]
case intro
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
a : F
ha : ↑(quadraticChar F) a = -1
⊢ IsNontrivial χ
[PROOFSTEP]
have hu : IsUnit a := by
  contrapose ha
  exact ne_of_eq_of_ne (map_nonunit (quadraticChar F) ha) (mt zero_eq_neg.mp one_ne_zero)
[GOAL]
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
a : F
ha : ↑(quadraticChar F) a = -1
⊢ IsUnit a
[PROOFSTEP]
contrapose ha
[GOAL]
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
a : F
ha : ¬IsUnit a
⊢ ¬↑(quadraticChar F) a = -1
[PROOFSTEP]
exact ne_of_eq_of_ne (map_nonunit (quadraticChar F) ha) (mt zero_eq_neg.mp one_ne_zero)
[GOAL]
case intro
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
a : F
ha : ↑(quadraticChar F) a = -1
hu : IsUnit a
⊢ IsNontrivial χ
[PROOFSTEP]
use hu.unit
[GOAL]
case h
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
a : F
ha : ↑(quadraticChar F) a = -1
hu : IsUnit a
⊢ ↑χ ↑(IsUnit.unit hu) ≠ 1
[PROOFSTEP]
simp only [IsUnit.unit_spec, ringHomComp_apply, eq_intCast, Ne.def, ha]
[GOAL]
case h
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
a : F
ha : ↑(quadraticChar F) a = -1
hu : IsUnit a
⊢ ¬↑(-1) = 1
[PROOFSTEP]
rw [Int.cast_neg, Int.cast_one]
[GOAL]
case h
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
a : F
ha : ↑(quadraticChar F) a = -1
hu : IsUnit a
⊢ ¬-1 = 1
[PROOFSTEP]
exact Ring.neg_one_ne_one_of_char_ne_two hF'
[GOAL]
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
hχ₁ : IsNontrivial χ
⊢ ↑(quadraticChar F) ↑(Fintype.card F') = ↑(quadraticChar F') (↑(↑(quadraticChar F) (-1)) * ↑(Fintype.card F))
[PROOFSTEP]
have hχ₂ : χ.IsQuadratic := IsQuadratic.comp (quadraticChar_isQuadratic F) _
[GOAL]
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
hχ₁ : IsNontrivial χ
hχ₂ : IsQuadratic χ
⊢ ↑(quadraticChar F) ↑(Fintype.card F') = ↑(quadraticChar F') (↑(↑(quadraticChar F) (-1)) * ↑(Fintype.card F))
[PROOFSTEP]
have h := Char.card_pow_card hχ₁ hχ₂ h hF'
[GOAL]
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h✝ : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
hχ₁ : IsNontrivial χ
hχ₂ : IsQuadratic χ
h : (↑χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = ↑χ ↑(Fintype.card F')
⊢ ↑(quadraticChar F) ↑(Fintype.card F') = ↑(quadraticChar F') (↑(↑(quadraticChar F) (-1)) * ↑(Fintype.card F))
[PROOFSTEP]
rw [← quadraticChar_eq_pow_of_char_ne_two' hF'] at h
[GOAL]
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h✝ : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
hχ₁ : IsNontrivial χ
hχ₂ : IsQuadratic χ
h : ↑(↑(quadraticChar F') (↑χ (-1) * ↑(Fintype.card F))) = ↑χ ↑(Fintype.card F')
⊢ ↑(quadraticChar F) ↑(Fintype.card F') = ↑(quadraticChar F') (↑(↑(quadraticChar F) (-1)) * ↑(Fintype.card F))
[PROOFSTEP]
exact (IsQuadratic.eq_of_eq_coe (quadraticChar_isQuadratic F') (quadraticChar_isQuadratic F) hF' h).symm
[GOAL]
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ ↑(quadraticChar F) ↑p = ↑(quadraticChar (ZMod p)) (↑(↑χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F))
[PROOFSTEP]
rw [← quadraticChar_neg_one hF]
[GOAL]
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ ↑(quadraticChar F) ↑p = ↑(quadraticChar (ZMod p)) (↑(↑(quadraticChar F) (-1)) * ↑(Fintype.card F))
[PROOFSTEP]
have h :=
  quadraticChar_card_card hF (ne_of_eq_of_ne (ringChar_zmod_n p) hp₁) (ne_of_eq_of_ne (ringChar_zmod_n p) hp₂.symm)
[GOAL]
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
h :
  ↑(quadraticChar F) ↑(Fintype.card (ZMod p)) =
    ↑(quadraticChar (ZMod p)) (↑(↑(quadraticChar F) (-1)) * ↑(Fintype.card F))
⊢ ↑(quadraticChar F) ↑p = ↑(quadraticChar (ZMod p)) (↑(↑(quadraticChar F) (-1)) * ↑(Fintype.card F))
[PROOFSTEP]
rwa [card p] at h
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare ↑p ↔ ↑(quadraticChar (ZMod p)) (↑(↑χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1
[PROOFSTEP]
classical
by_cases hFp : ringChar F = p
· rw [show (p : F) = 0 by rw [← hFp]; exact ringChar.Nat.cast_ringChar]
  simp only [isSquare_zero, Ne.def, true_iff_iff, map_mul]
  obtain ⟨n, _, hc⟩ := FiniteField.card F (ringChar F)
  have hchar : ringChar F = ringChar (ZMod p) := by rw [hFp]; exact (ringChar_zmod_n p).symm
  conv => enter [1, 1, 2]; rw [hc, Nat.cast_pow, map_pow, hchar, map_ringChar]
  simp only [zero_pow n.pos, mul_zero, zero_eq_neg, one_ne_zero, not_false_iff]
· rw [← Iff.not_left (@quadraticChar_neg_one_iff_not_isSquare F _ _ _ _), quadraticChar_odd_prime hF hp]
  exact hFp
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare ↑p ↔ ↑(quadraticChar (ZMod p)) (↑(↑χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1
[PROOFSTEP]
by_cases hFp : ringChar F = p
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ IsSquare ↑p ↔ ↑(quadraticChar (ZMod p)) (↑(↑χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1
[PROOFSTEP]
rw [show (p : F) = 0 by rw [← hFp]; exact ringChar.Nat.cast_ringChar]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ ↑p = 0
[PROOFSTEP]
rw [← hFp]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ ↑(ringChar F) = 0
[PROOFSTEP]
exact ringChar.Nat.cast_ringChar
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ IsSquare 0 ↔ ↑(quadraticChar (ZMod p)) (↑(↑χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1
[PROOFSTEP]
simp only [isSquare_zero, Ne.def, true_iff_iff, map_mul]
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ ¬↑(quadraticChar (ZMod p)) ↑(↑χ₄ ↑(Fintype.card F)) * ↑(quadraticChar (ZMod p)) ↑(Fintype.card F) = -1
[PROOFSTEP]
obtain ⟨n, _, hc⟩ := FiniteField.card F (ringChar F)
[GOAL]
case pos.intro.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
⊢ ¬↑(quadraticChar (ZMod p)) ↑(↑χ₄ ↑(Fintype.card F)) * ↑(quadraticChar (ZMod p)) ↑(Fintype.card F) = -1
[PROOFSTEP]
have hchar : ringChar F = ringChar (ZMod p) := by rw [hFp]; exact (ringChar_zmod_n p).symm
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = ringChar (ZMod p)
[PROOFSTEP]
rw [hFp]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
⊢ p = ringChar (ZMod p)
[PROOFSTEP]
exact (ringChar_zmod_n p).symm
[GOAL]
case pos.intro.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
hchar : ringChar F = ringChar (ZMod p)
⊢ ¬↑(quadraticChar (ZMod p)) ↑(↑χ₄ ↑(Fintype.card F)) * ↑(quadraticChar (ZMod p)) ↑(Fintype.card F) = -1
[PROOFSTEP]
conv => enter [1, 1, 2]; rw [hc, Nat.cast_pow, map_pow, hchar, map_ringChar]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
hchar : ringChar F = ringChar (ZMod p)
| ¬↑(quadraticChar (ZMod p)) ↑(↑χ₄ ↑(Fintype.card F)) * ↑(quadraticChar (ZMod p)) ↑(Fintype.card F) = -1
[PROOFSTEP]
enter [1, 1, 2]; rw [hc, Nat.cast_pow, map_pow, hchar, map_ringChar]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
hchar : ringChar F = ringChar (ZMod p)
| ¬↑(quadraticChar (ZMod p)) ↑(↑χ₄ ↑(Fintype.card F)) * ↑(quadraticChar (ZMod p)) ↑(Fintype.card F) = -1
[PROOFSTEP]
enter [1, 1, 2]; rw [hc, Nat.cast_pow, map_pow, hchar, map_ringChar]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
hchar : ringChar F = ringChar (ZMod p)
| ¬↑(quadraticChar (ZMod p)) ↑(↑χ₄ ↑(Fintype.card F)) * ↑(quadraticChar (ZMod p)) ↑(Fintype.card F) = -1
[PROOFSTEP]
enter [1, 1, 2]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
hchar : ringChar F = ringChar (ZMod p)
| ↑(quadraticChar (ZMod p)) ↑(Fintype.card F)
[PROOFSTEP]
rw [hc, Nat.cast_pow, map_pow, hchar, map_ringChar]
[GOAL]
case pos.intro.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
hchar : ringChar F = ringChar (ZMod p)
⊢ ¬↑(quadraticChar (ZMod p)) ↑(↑χ₄ ↑(Fintype.card F)) * 0 ^ ↑n = -1
[PROOFSTEP]
simp only [zero_pow n.pos, mul_zero, zero_eq_neg, one_ne_zero, not_false_iff]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ¬ringChar F = p
⊢ IsSquare ↑p ↔ ↑(quadraticChar (ZMod p)) (↑(↑χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1
[PROOFSTEP]
rw [← Iff.not_left (@quadraticChar_neg_one_iff_not_isSquare F _ _ _ _), quadraticChar_odd_prime hF hp]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ¬ringChar F = p
⊢ ringChar F ≠ p
[PROOFSTEP]
exact hFp