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
a : F
ha : a ≠ 0
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
sq_eq_one_iff.1 <| quadraticChar_sq_one ha

Premises used: sq_eq_one_iff, quadraticChar_sq_one, Iff.mp
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a ≠ 0
h : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
rw : ¬Eq (α := ℤ) (-1) 1
⊢ ¬Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a ≠ 0
h : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
⊢ ¬Eq (α := ℤ) (-1) 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
pos : ∀ (ha : a = 0), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ) ↔ ¬IsSquare a
neg : ∀ (ha : ¬a = 0), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ) ↔ ¬IsSquare a
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ) ↔ ¬IsSquare a

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a = 0
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ) ↔ ¬IsSquare a

Tactic:
simp only [ha, MulChar.map_zero, zero_eq_neg, one_ne_zero, IsSquare.zero, not_true]

Premises used: zero_eq_neg, IsSquare.zero, not_true, one_ne_zero, MulChar.map_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : ¬a = 0
neg : ¬Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ↔ ¬IsSquare a
neg₁ neg₂ : ¬IsSquare a ↔ ¬IsSquare a
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ) ↔ ¬IsSquare a

Tactic:
rw [quadraticChar_eq_neg_one_iff_not_one ha, quadraticChar_one_iff_isSquare ha]

Premises used: quadraticChar_eq_neg_one_iff_not_one, quadraticChar_one_iff_isSquare
-- 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), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
(FiniteField.exists_nonsquare hF).imp fun _ h₁ ↦ quadraticChar_neg_one_iff_not_isSquare.mpr h₁

Premises used: Iff.mpr, Exists.imp, FiniteField.exists_nonsquare, quadraticChar_neg_one_iff_not_isSquare
-- 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ˣ), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑a : F) : ℤ) (-1 : ℤ)

Tactic:
(fun ⟨a, ha⟩ ↦ ⟨IsUnit.unit ?_, ha⟩) (quadraticChar_exists_neg_one hF)

Premises used: quadraticChar_exists_neg_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
refine :
  (∃ (a : F), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)) →
    ∀ (a : F) (ha : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)), IsUnit a
⊢ ∃ (a : Fˣ), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑a : F) : ℤ) (-1 : ℤ)

Tactic:
refine (fun ⟨a, ha⟩ ↦ ⟨IsUnit.unit ?_, ha⟩) (quadraticChar_exists_neg_one hF)

Premises used: quadraticChar_exists_neg_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
h : ∃ (a : F), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
a : F
ha : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
contrapose : ∀ (ha : ¬IsUnit a), ¬Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
⊢ IsUnit a

Tactic:
contrapose ha
-- 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 : ∃ (a : F), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
a : F
ha : ¬IsUnit a
⊢ ¬Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
ne_of_eq_of_ne ((quadraticChar F).map_nonunit ha) (mt zero_eq_neg.mp one_ne_zero)

Premises used: ne_of_eq_of_ne, zero_eq_neg, quadraticChar, mt, Iff.mp, MulChar.map_nonunit, 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 : ∃ (a : F), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
a : F
ha : ¬IsUnit a
⊢ ¬Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
exact ne_of_eq_of_ne ((quadraticChar F).map_nonunit ha) (mt zero_eq_neg.mp one_ne_zero)

Premises used: ne_of_eq_of_ne, zero_eq_neg, quadraticChar, mt, Iff.mp, MulChar.map_nonunit, 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
a : F
ha : a ≠ 0
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)

Tactic:
quadraticCharFun_eq_one_of_char_two hF ha

Premises used: quadraticCharFun_eq_one_of_char_two, quadraticCharFun, ite
-- 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
ha : a ≠ 0
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (if a ^ (Fintype.card F / 2) = 1 then 1 else -1 : ℤ)

Tactic:
quadraticCharFun_eq_pow_of_char_ne_two hF ha

Premises used: quadraticCharFun, quadraticCharFun_eq_pow_of_char_ne_two, ite
-- 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
pos : ∀ (ha : a = 0), (↑((quadraticChar F : (a : F) → ℤ) a) : F) = a ^ (Fintype.card F / 2)
neg : ∀ (ha : ¬a = 0), (↑((quadraticChar F : (a : F) → ℤ) a) : F) = a ^ (Fintype.card F / 2)
⊢ (↑((quadraticChar F : (a : F) → ℤ) a) : F) = a ^ (Fintype.card F / 2)

Tactic:
by_cases ha : a = 0
-- 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
ha : a = 0
⊢ 0 < Fintype.card F / 2

Tactic:
have : 0 < Fintype.card F / 2 := Nat.div_pos Fintype.one_lt_card two_pos
-- 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
ha : a = 0
this : 0 < Fintype.card F / 2
⊢ (↑((quadraticChar F : (a : F) → ℤ) a) : F) = a ^ (Fintype.card F / 2)

Tactic:
simp only [ha, quadraticChar_apply, quadraticCharFun_zero, Int.cast_zero, zero_pow this.ne']

Premises used: Int.cast_zero, LT.lt.ne', quadraticChar_apply, quadraticCharFun_zero, zero_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
a : F
ha : ¬a = 0
neg : (↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) : F) = a ^ (Fintype.card F / 2)
⊢ (↑((quadraticChar F : (a : F) → ℤ) a) : F) = a ^ (Fintype.card F / 2)

Tactic:
rw [quadraticChar_eq_pow_of_char_ne_two hF ha]

Premises used: quadraticChar_eq_pow_of_char_ne_two
-- 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
ha : ¬a = 0
pos :
  ∀ (ha' : a ^ (Fintype.card F / 2) = 1),
    (↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) : F) = a ^ (Fintype.card F / 2)
neg :
  ∀ (ha' : ¬a ^ (Fintype.card F / 2) = 1),
    (↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) : F) = a ^ (Fintype.card F / 2)
⊢ (↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) : F) = a ^ (Fintype.card F / 2)

Tactic:
by_cases ha' : a ^ (Fintype.card F / 2) = 1

Premises used: Fintype.card, HDiv.hDiv, OfNat.ofNat
-- 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
ha : ¬a = 0
ha' : a ^ (Fintype.card F / 2) = 1
⊢ (↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) : F) = a ^ (Fintype.card F / 2)

Tactic:
simp only [ha', if_true, Int.cast_one]

Premises used: if_true, Int.cast_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
a : F
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
⊢ a ^ (Fintype.card F / 2) = -1

Tactic:
have ha'' := Or.resolve_left (FiniteField.pow_dichotomy hF ha) ha'
-- 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
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
ha'' : a ^ (Fintype.card F / 2) = -1
neg : Eq.{u_1 + 1} (α := F) (-1) 1 → Eq.{u_1 + 1} (α := F) 1 (-1)
⊢ (↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) : F) = a ^ (Fintype.card F / 2)

Tactic:
simp only [ha'', Int.cast_ite, Int.cast_one, Int.cast_neg, ite_eq_right_iff]

Premises used: Int.cast_neg, ite_eq_right_iff, Int.cast_one, Int.cast_ite
-- 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
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
ha'' : a ^ (Fintype.card F / 2) = -1
⊢ Eq.{u_1 + 1} (α := F) (-1) 1 → Eq.{u_1 + 1} (α := F) 1 (-1)

Tactic:
Eq.symm

Premises used: Eq.symm
-- 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
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
ha'' : a ^ (Fintype.card F / 2) = -1
⊢ Eq.{u_1 + 1} (α := F) (-1) 1 → Eq.{u_1 + 1} (α := F) 1 (-1)

Tactic:
exact Eq.symm

Premises used: Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
pos :
  ∀ (ha : a = 0),
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
        Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
neg :
  ∀ (ha : ¬a = 0),
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
        Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
      Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a = 0
pos : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
      Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
left
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a = 0
pos : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (0 : ℤ)

Tactic:
rw [ha]
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a = 0
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) 0 : ℤ) (0 : ℤ)

Tactic:
quadraticChar_zero

Premises used: quadraticChar_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a = 0
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) 0 : ℤ) (0 : ℤ)

Tactic:
exact quadraticChar_zero

Premises used: quadraticChar_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : ¬a = 0
neg :
  Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
      Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
right
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : ¬a = 0
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
quadraticChar_dichotomy ha

Premises used: quadraticChar_dichotomy
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : ¬a = 0
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
exact quadraticChar_dichotomy ha

Premises used: quadraticChar_dichotomy
-- 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
rcases :
  ∀ (a : Fˣ) (ha : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑a : F) : ℤ) (-1 : ℤ)),
    Ne (α := MulChar F ℤ) (quadraticChar F) 1
⊢ Ne (α := MulChar F ℤ) (quadraticChar F) 1

Tactic:
rcases quadraticChar_exists_neg_one' hF with ⟨a, ha⟩

Premises used: quadraticChar_exists_neg_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
a : Fˣ
ha : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑a : F) : ℤ) (-1 : ℤ)
hχ : Eq (α := MulChar F ℤ) (quadraticChar F) 1
⊢ False

Tactic:
simp only [hχ, one_apply a.isUnit, reduceCtorEq] at ha

Premises used: reduceCtorEq, MulChar.one_apply, Units.isUnit
-- 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
pos :
  ∀ (h₀ : a = 0),
    (↑(card.{u_1} (α := F) (Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a})) : ℤ) =
      HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
neg :
  ∀ (h₀ : ¬a = 0),
    (↑(card.{u_1} (α := F) (Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a})) : ℤ) =
      HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
⊢ (↑(card.{u_1} (α := F) (Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a})) : ℤ) =
    HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)

Tactic:
by_cases h₀ : a = 0
-- 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
⊢ (↑(card.{u_1} (α := F) (Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a})) : ℤ) =
    HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)

Tactic:
simp only [h₀, sq_eq_zero_iff, Set.setOf_eq_eq_singleton, Set.toFinset_card,
    Set.card_singleton, Int.natCast_succ, Int.ofNat_zero, MulChar.map_zero]

Premises used: Set.setOf_eq_eq_singleton, Set.toFinset_card, Int.ofNat_zero, Int.natCast_succ, Set.card_singleton, MulChar.map_zero, sq_eq_zero_iff
-- 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
neg :
  let s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a};
  (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
⊢ (↑(card.{u_1} (α := F) (Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a})) : ℤ) =
    HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)

Tactic:
set s := {x : F | x ^ 2 = a}.toFinset

Premises used: setOf, Set.toFinset, HPow.hPow, OfNat.ofNat, Eq
-- 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}
pos : ∀ (h : IsSquare a), (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
neg : ∀ (h : ¬IsSquare a), (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)

Tactic:
by_cases h : IsSquare a

Premises used: IsSquare
-- 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
pos : (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) 1 1
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)

Tactic:
rw [(quadraticChar_one_iff_isSquare h₀).mpr h]

Premises used: Iff.mpr, quadraticChar_one_iff_isSquare
-- 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
pos : ∀ (b : F) (h : a = b * b), (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) 1 1
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) 1 1

Tactic:
rcases h with ⟨b, h⟩
-- 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}
b : F
h : a = b * b
⊢ ¬b = 0

Tactic:
rw [h, mul_self_eq_zero] at h₀

Premises used: mul_self_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}
b : F
h : a = b * b
h₁ : ¬b = 0
⊢ a = b * b

Tactic:
rw [h, mul_self_eq_zero] at h₀

Premises used: mul_self_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
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
h₁ : ∀ (a : F), a ∈ s ↔ a ∈ [b, -b].toFinset
⊢ s = [b, -b].toFinset

Tactic:
ext1
-- 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
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
a_1 : F
h₁ : ∀ (h : a = HPow.hPow (β := ℕ) b 2) (a : F), a ∈ s ↔ a ∈ [b, -b].toFinset
⊢ a_1 ∈ s ↔ a_1 ∈ [b, -b].toFinset

Tactic:
rw [← pow_two] at h

Premises used: pow_two
-- 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
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
b : F
h₀ : ¬b = 0
h : a = HPow.hPow (β := ℕ) b 2
a_1 : F
h₁ : HPow.hPow (β := ℕ) a_1 2 = HPow.hPow (β := ℕ) b 2 ↔ a_1 = b ∨ a_1 = -b
⊢ a_1 ∈ s ↔ a_1 ∈ [b, -b].toFinset

Tactic:
simp_rw [s, Set.toFinset_setOf, mem_filter_univ, h, List.toFinset_cons, List.toFinset_nil,
          insert_empty_eq, mem_insert, mem_singleton]

Premises used: Finset.mem_singleton, Finset.mem_filter_univ, Finset.mem_insert, LawfulSingleton.insert_empty_eq, List.toFinset_cons, List.toFinset_nil, Set.toFinset_setOf
-- 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
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
b : F
h₀ : ¬b = 0
h : a = HPow.hPow (β := ℕ) b 2
a_1 : F
⊢ HPow.hPow (β := ℕ) a_1 2 = HPow.hPow (β := ℕ) b 2 ↔ a_1 = b ∨ a_1 = -b

Tactic:
sq_eq_sq_iff_eq_or_eq_neg

Premises used: sq_eq_sq_iff_eq_or_eq_neg
-- 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
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
b : F
h₀ : ¬b = 0
h : a = HPow.hPow (β := ℕ) b 2
a_1 : F
⊢ HPow.hPow (β := ℕ) a_1 2 = HPow.hPow (β := ℕ) b 2 ↔ a_1 = b ∨ a_1 = -b

Tactic:
exact sq_eq_sq_iff_eq_or_eq_neg

Premises used: sq_eq_sq_iff_eq_or_eq_neg
-- 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
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
⊢ s = [b, -b].toFinset

Tactic:
have h₁ : s = [b, -b].toFinset := by
        ext1
        rw [← pow_two] at h
        simp_rw [s, Set.toFinset_setOf, mem_filter_univ, h, List.toFinset_cons, List.toFinset_nil,
          insert_empty_eq, mem_insert, mem_singleton]
        exact sq_eq_sq_iff_eq_or_eq_neg
-- 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
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
h₁ : s = [b, -b].toFinset
pos : #s = HAdd.hAdd (α := ℕ) 1 1
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) 1 1

Tactic:
norm_cast
-- 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
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
h₁ : s = [b, -b].toFinset
pos : card (α := F) (insert b (insert (-b) ∅)) = HAdd.hAdd (α := ℕ) 1 1
⊢ #s = HAdd.hAdd (α := ℕ) 1 1

Tactic:
rw [h₁, List.toFinset_cons, List.toFinset_cons, List.toFinset_nil]

Premises used: List.toFinset_cons, List.toFinset_nil
-- 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
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
h₁ : s = [b, -b].toFinset
⊢ card (α := F) (insert b (insert (-b) ∅)) = HAdd.hAdd (α := ℕ) 1 1

Tactic:
card_pair (Ne.symm (mt (Ring.eq_self_iff_eq_zero_of_char_ne_two hF).mp h₀))

Premises used: mt, Multiset.cons, Ne.symm, Multiset.ofList, Iff.mp, Finset.card_pair, Multiset.ndinsert, Ring.eq_self_iff_eq_zero_of_char_ne_two, ite
-- 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
s : Finset F := Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
h₁ : s = [b, -b].toFinset
⊢ card (α := F) (insert b (insert (-b) ∅)) = HAdd.hAdd (α := ℕ) 1 1

Tactic:
exact card_pair (Ne.symm (mt (Ring.eq_self_iff_eq_zero_of_char_ne_two hF).mp h₀))

Premises used: mt, Ne.symm, Iff.mp, Finset.card_pair, Ring.eq_self_iff_eq_zero_of_char_ne_two
-- 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 : (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (-1) 1
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)

Tactic:
rw [quadraticChar_neg_one_iff_not_isSquare.mpr h]

Premises used: Iff.mpr, quadraticChar_neg_one_iff_not_isSquare