awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
h : ¬IsSquare a
neg : ∀ (x : F), x ∉ s
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (-1) 1

Tactic:
simp only [neg_add_cancel, Int.natCast_eq_zero, card_eq_zero, eq_empty_iff_forall_notMem]

Premises used: Finset.eq_empty_iff_forall_notMem, Int.natCast_eq_zero, neg_add_cancel, Finset.card_eq_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
h : ¬IsSquare a
⊢ ∀ (x : F), x ∉ s

Tactic:
simpa [s, isSquare_iff_exists_sq, eq_comm] using h

Premises used: eq_comm, isSquare_iff_exists_sq
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
⊢ Eq (α := ℤ) (∑ a : F, (quadraticChar F : (a : F) → ℤ) a) 0

Tactic:
sum_eq_zero_of_ne_one (quadraticChar_ne_one hF)

Premises used: quadraticChar_ne_one, MulChar.sum_eq_zero_of_ne_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-1) : ℤ)
    (if HPow.hPow (α := F) (-1) (Fintype.card F / 2) = 1 then 1 else -1 : ℤ)

Tactic:
have h := quadraticChar_eq_pow_of_char_ne_two hF (neg_ne_zero.mpr one_ne_zero)
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-1) : ℤ)
    (if HPow.hPow (α := F) (-1) (Fintype.card F / 2) = 1 then 1 else -1 : ℤ)
rw : (if HPow.hPow (α := F) (-1) (Fintype.card F / 2) = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (Fintype.card F / 2)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-1) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4) : ℤ)

Tactic:
rw [h, χ₄_eq_neg_one_pow (FiniteField.odd_card_of_char_ne_two hF)]

Premises used: FiniteField.odd_card_of_char_ne_two, ZMod.χ₄_eq_neg_one_pow
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-1) : ℤ)
    (if HPow.hPow (α := F) (-1) (Fintype.card F / 2) = 1 then 1 else -1 : ℤ)
generalize : ∀ (n : ℕ), (if HPow.hPow (α := F) (-1) n = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) n
⊢ (if HPow.hPow (α := F) (-1) (Fintype.card F / 2) = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (Fintype.card F / 2)

Tactic:
generalize Fintype.card F / 2 = n

Premises used: Fintype.card
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-1) : ℤ)
    (if HPow.hPow (α := F) (-1) (Fintype.card F / 2) = 1 then 1 else -1 : ℤ)
n : ℕ
inl : ∀ (h₂ : Even n), (if HPow.hPow (α := F) (-1) n = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) n
inr : ∀ (h₂ : Odd n), (if HPow.hPow (α := F) (-1) n = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) n
⊢ (if HPow.hPow (α := F) (-1) n = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) n

Tactic:
rcases Nat.even_or_odd n with h₂ | h₂

Premises used: Nat.even_or_odd
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-1) : ℤ)
    (if HPow.hPow (α := F) (-1) (Fintype.card F / 2) = 1 then 1 else -1 : ℤ)
n : ℕ
h₂ : Even n
⊢ (if HPow.hPow (α := F) (-1) n = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) n

Tactic:
simp only [Even.neg_one_pow h₂, if_true]

Premises used: if_true, Even.neg_one_pow
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-1) : ℤ)
    (if HPow.hPow (α := F) (-1) (Fintype.card F / 2) = 1 then 1 else -1 : ℤ)
n : ℕ
h₂ : Odd n
⊢ (if HPow.hPow (α := F) (-1) n = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) n

Tactic:
simp only [Odd.neg_one_pow h₂, Ring.neg_one_ne_one_of_char_ne_two hF, ite_false]

Premises used: Ring.neg_one_ne_one_of_char_ne_two, ite_false, Odd.neg_one_pow
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
pos : ∀ (hF : ringChar F = 2), IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
neg : ∀ (hF : ¬ringChar F = 2), IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
⊢ IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3

Tactic:
by_cases hF : ringChar F = 2

Premises used: ringChar
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
pos : ¬Fintype.card F % 4 = 3
⊢ IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3

Tactic:
simp only [FiniteField.isSquare_of_char_two hF, Ne, true_iff]

Premises used: true_iff, Ne, FiniteField.isSquare_of_char_two
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
⊢ ¬Fintype.card F % 4 = 3

Tactic:
fun hf ↦
      one_ne_zero <|
        (Nat.odd_of_mod_four_eq_three hf).symm.trans <| FiniteField.even_card_of_char_two hF

Premises used: FiniteField.even_card_of_char_two, Nat.odd_of_mod_four_eq_three, one_ne_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
⊢ ¬Fintype.card F % 4 = 3

Tactic:
exact fun hf ↦
      one_ne_zero <|
        (Nat.odd_of_mod_four_eq_three hf).symm.trans <| FiniteField.even_card_of_char_two hF

Premises used: FiniteField.even_card_of_char_two, Nat.odd_of_mod_four_eq_three, one_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
⊢ Fintype.card F % 2 = 1

Tactic:
have h₁ := FiniteField.odd_card_of_char_ne_two hF
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
neg : Eq (α := ℤ) (if Eq (α := ℕ) 1 0 then 0 else if Fintype.card F % 4 = 1 then 1 else -1) 1 ↔ Fintype.card F % 4 ≠ 3
⊢ IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3

Tactic:
rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (one_ne_zero' F)),
      quadraticChar_neg_one hF, χ₄_nat_eq_if_mod_four, h₁]

Premises used: Iff.mpr, one_ne_zero', neg_ne_zero, quadraticChar_neg_one, quadraticChar_one_iff_isSquare, ZMod.χ₄_nat_eq_if_mod_four
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ Eq (α := ℤ) (if Eq (α := ℕ) 1 0 then 0 else if Fintype.card F % 4 = 1 then 1 else -1) 1 ↔ Fintype.card F % 4 ≠ 3

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
pos : ∀ (hF : ringChar F = 2), IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
neg neg₁ : ∀ (hF : ¬ringChar F = 2), IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
⊢ IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3

Tactic:
classical -- suggested by the linter (instead of `[DecidableEq F]`)
  by_cases hF : ringChar F = 2
  · simp only [FiniteField.isSquare_of_char_two hF, Ne, true_iff]
    exact fun hf ↦
      one_ne_zero <|
        (Nat.odd_of_mod_four_eq_three hf).symm.trans <| FiniteField.even_card_of_char_two hF
  · have h₁ := FiniteField.odd_card_of_char_ne_two hF
    rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (one_ne_zero' F)),
      quadraticChar_neg_one hF, χ₄_nat_eq_if_mod_four, h₁]
    lia

Premises used: true_iff, Ne, ringChar, ZMod.χ₄_nat_eq_if_mod_four
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) 2 : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)

Tactic:
IsQuadratic.eq_of_eq_coe (quadraticChar_isQuadratic F) isQuadratic_χ₈ hF
    ((quadraticChar_eq_pow_of_char_ne_two' hF 2).trans (FiniteField.two_pow_card hF))

Premises used: quadraticChar_isQuadratic, FiniteField.two_pow_card, ZMod.isQuadratic_χ₈, MulChar.IsQuadratic.eq_of_eq_coe, quadraticChar_eq_pow_of_char_ne_two', OfNat.ofNat, Eq.trans
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
pos : ∀ (hF : ringChar F = 2), IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
neg : ∀ (hF : ¬ringChar F = 2), IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
⊢ IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
by_cases hF : ringChar F = 2

Premises used: ringChar
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
⊢ Fintype.card F % 2 = 0

Tactic:
have h := FiniteField.even_card_of_char_two hF
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
pos : Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
⊢ IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
simp only [FiniteField.isSquare_of_char_two hF, true_iff]

Premises used: true_iff, FiniteField.isSquare_of_char_two
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
⊢ Fintype.card F % 2 = 1

Tactic:
have h := FiniteField.odd_card_of_char_ne_two hF
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
neg :
  Eq (α := ℤ) (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
⊢ IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
rw [← quadraticChar_one_iff_isSquare (Ring.two_ne_zero hF), quadraticChar_two hF,
      χ₈_nat_eq_if_mod_eight]

Premises used: quadraticChar_two, Ring.two_ne_zero, ZMod.χ₈_nat_eq_if_mod_eight, quadraticChar_one_iff_isSquare
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ Eq (α := ℤ) (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

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
pos : ∀ (hF : ringChar F = 2), IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
neg neg₁ : ∀ (hF : ¬ringChar F = 2), IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
⊢ IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
classical
  by_cases hF : ringChar F = 2
  · have h := FiniteField.even_card_of_char_two hF
    simp only [FiniteField.isSquare_of_char_two hF, true_iff]
    lia
  · 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]
    lia

Premises used: true_iff, ringChar, ZMod.χ₈_nat_eq_if_mod_eight
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
⊢ -2 = HMul.hMul (α := F) (-1) 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
⊢ Dvd.dvd (α := ℕ) 4 8

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
rw : -2 = HMul.hMul (α := F) (-1) 2
rw₁ :
  Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (HMul.hMul (α := F) (-1) 2) : ℤ)
    ((χ₈' : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)
rw₂ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) (-1) : ℤ) ((quadraticChar F : (a : F) → ℤ) 2 : ℤ) =
    (χ₈' : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)
rw₃ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) (-1) : ℤ) ((quadraticChar F : (a : F) → ℤ) 2 : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (ZMod.cast (n := 8) (↑(Fintype.card F) : ZMod 8)) : ℤ)
      ((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)
rw₄ :
  HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4) : ℤ)
      ((quadraticChar F : (a : F) → ℤ) 2 : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (ZMod.cast (n := 8) (↑(Fintype.card F) : ZMod 8)) : ℤ)
      ((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)
rw₅ :
  HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4) : ℤ)
      ((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (ZMod.cast (n := 8) (↑(Fintype.card F) : ZMod 8)) : ℤ)
      ((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)
rw₆ rw₇ :
  HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4) : ℤ)
      ((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4) : ℤ)
      ((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-2) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)

Tactic:
rw [(by simp : (-2 : F) = -1 * 2), map_mul, χ₈'_eq_χ₄_mul_χ₈, quadraticChar_neg_one hF,
    quadraticChar_two hF, @cast_natCast _ (ZMod 4) _ _ _ (by decide : 4 ∣ 8)]

Premises used: quadraticChar_two, ZMod.χ₈'_eq_χ₄_mul_χ₈, ZMod.cast_natCast, map_mul, quadraticChar_neg_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
pos : ∀ (hF : ringChar F = 2), IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
neg : ∀ (hF : ¬ringChar F = 2), IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
⊢ IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
by_cases hF : ringChar F = 2

Premises used: ringChar
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
pos : Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
⊢ IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
simp only [FiniteField.isSquare_of_char_two hF, true_iff]

Premises used: true_iff, FiniteField.isSquare_of_char_two
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
neg :
  Eq (α := ℤ) (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
⊢ IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (Ring.two_ne_zero hF)),
      quadraticChar_neg_two hF, χ₈'_nat_eq_if_mod_eight]

Premises used: Iff.mpr, Ring.two_ne_zero, ZMod.χ₈'_nat_eq_if_mod_eight, quadraticChar_neg_two, neg_ne_zero, quadraticChar_one_iff_isSquare
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ Eq (α := ℤ) (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

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
pos : ∀ (hF : ringChar F = 2), IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
neg neg₁ : ∀ (hF : ¬ringChar F = 2), IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
⊢ IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
classical
  by_cases hF : ringChar F = 2
  · have h := FiniteField.even_card_of_char_two hF
    simp only [FiniteField.isSquare_of_char_two hF, true_iff]
    lia
  · 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]
    lia

Premises used: ZMod.χ₈'_nat_eq_if_mod_eight, true_iff, ringChar
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst_3 : Field F'
inst_4 : Fintype F'
inst_5 : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
obtain : ∀ (a : Fˣ) (ha : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑a : F) : ℤ) (-1 : ℤ)), χ ≠ 1
⊢ χ ≠ 1

Tactic:
obtain ⟨a, ha⟩ := quadraticChar_exists_neg_one' hF

Premises used: quadraticChar_exists_neg_one'
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst_3 : Field F'
inst_4 : Fintype F'
inst_5 : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
a : Fˣ
ha : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑a : F) : ℤ) (-1 : ℤ)
⊢ χ ≠ 1

Tactic:
ne_one_iff.mpr ⟨a, ?_⟩

Premises used: Iff.mpr, MulChar.ne_one_iff, Exists.intro
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst_3 : Field F'
inst_4 : Fintype F'
inst_5 : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
a : Fˣ
ha : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑a : F) : ℤ) (-1 : ℤ)
refine : Ne.{u_2 + 1} (α := F') ((χ : (a : F) → F') (↑a : F) : F') (1 : F')
⊢ χ ≠ 1

Tactic:
refine ne_one_iff.mpr ⟨a, ?_⟩

Premises used: Iff.mpr, MulChar.ne_one_iff, Exists.intro
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst_3 : Field F'
inst_4 : Fintype F'
inst_5 : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
a : Fˣ
ha : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑a : F) : ℤ) (-1 : ℤ)
⊢ Ne.{u_2 + 1} (α := F') ((χ : (a : F) → F') (↑a : F) : F') (1 : F')

Tactic:
simpa only [ringHomComp_apply, ha, eq_intCast, Int.cast_neg, Int.cast_one, χ] using
      Ring.neg_one_ne_one_of_char_ne_two hF'

Premises used: Int.cast_neg, Ring.neg_one_ne_one_of_char_ne_two, MulChar.ringHomComp_apply, eq_intCast, Int.cast_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst_3 : Field F'
inst_4 : Fintype F'
inst_5 : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
⊢ χ ≠ 1

Tactic:
have hχ₁ : χ ≠ 1 := by
    obtain ⟨a, ha⟩ := quadraticChar_exists_neg_one' hF
    refine ne_one_iff.mpr ⟨a, ?_⟩
    simpa only [ringHomComp_apply, ha, eq_intCast, Int.cast_neg, Int.cast_one, χ] using
      Ring.neg_one_ne_one_of_char_ne_two hF'
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst_3 : Field F'
inst_4 : Fintype F'
inst_5 : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
hχ₁ : χ ≠ 1
⊢ HMul.hMul (α := F') (β := F') ((χ : (a : F) → F') (-1) : F') ((↑(Fintype.card F) : F') : F') ^ (Fintype.card F' / 2) =
    (χ : (a : F) → F') (↑(Fintype.card F') : F)

Tactic:
have h := Char.card_pow_card hχ₁ ((quadraticChar_isQuadratic F).comp _) h hF'
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst_3 : Field F'
inst_4 : Fintype F'
inst_5 : DecidableEq F'
hF' : ringChar F' ≠ 2
h_1 : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
hχ₁ : χ ≠ 1
h :
  HMul.hMul (α := F') (β := F') ((χ : (a : F) → F') (-1) : F') ((↑(Fintype.card F) : F') : F') ^ (Fintype.card F' / 2) =
    (χ : (a : F) → F') (↑(Fintype.card F') : F)
⊢ Eq.{u_2 + 1} (α := F')
    ((↑((quadraticChar F' : (a : F') → ℤ)
            (HMul.hMul (α := F') (β := F') ((χ : (a : F) → F') (-1) : F') ((↑(Fintype.card F) : F') : F'))) :
        F') :
      F')
    ((χ : (a : F) → F') (↑(Fintype.card F') : F) : F')

Tactic:
rw [← quadraticChar_eq_pow_of_char_ne_two' hF'] at h

Premises used: quadraticChar_eq_pow_of_char_ne_two'
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst_3 : Field F'
inst_4 : Fintype F'
inst_5 : DecidableEq F'
hF' : ringChar F' ≠ 2
h_1 : ringChar F' ≠ ringChar F
χ : MulChar F F' := ringHomComp (quadraticChar F) (algebraMap ℤ F')
hχ₁ : χ ≠ 1
h :
  Eq.{u_2 + 1} (α := F')
    ((↑((quadraticChar F' : (a : F') → ℤ)
            (HMul.hMul (α := F') (β := F') ((χ : (a : F) → F') (-1) : F') ((↑(Fintype.card F) : F') : F'))) :
        F') :
      F')
    ((χ : (a : F) → F') (↑(Fintype.card F') : F) : F')
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑(Fintype.card F') : F) : ℤ)
    ((quadraticChar F' : (a : F') → ℤ)
        (HMul.hMul (α := F') (↑((quadraticChar F : (a : F) → ℤ) (-1)) : F') (↑(Fintype.card F) : F')) :
      ℤ)

Tactic:
(IsQuadratic.eq_of_eq_coe (quadraticChar_isQuadratic F')
    (quadraticChar_isQuadratic F) hF' h).symm

Premises used: quadraticChar_isQuadratic, MulChar.IsQuadratic.eq_of_eq_coe, Eq.symm