awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a ≠ 0
rwa : HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) = 1
rwa₁ : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (a * a) : ℤ) (1 : ℤ)
rwa₂ : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (HPow.hPow (β := ℕ) a 2) : ℤ) (1 : ℤ)
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) 2 = 1
have rwa₃ : Eq (α := ℤ) 1 1
Tactic: rwa [pow_two, ← map_mul, ← pow_two, quadraticChar_sq_one']
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
have rw : ¬Eq (α := ℤ) (-1) 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ) ↔ ¬IsSquare a
have pos : ∀ (ha : a = 0), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ) ↔ ¬IsSquare a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ) ↔ ¬IsSquare a
have neg : ∀ (ha : ¬a = 0), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ) ↔ ¬IsSquare a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
have neg : ¬Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ↔ ¬IsSquare a
Tactic: rw [quadraticChar_eq_neg_one_iff_not_one ha, quadraticChar_one_iff_isSquare ha]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ) ↔ ¬IsSquare a
have neg₁ : ¬IsSquare a ↔ ¬IsSquare a
Tactic: rw [quadraticChar_eq_neg_one_iff_not_one ha, quadraticChar_one_iff_isSquare ha]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℤ)
have refine : (∃ (a : F), Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)) →
  ∀ (a : F) (ha : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)), IsUnit a
Tactic: refine (fun ⟨a, ha⟩ ↦ ⟨IsUnit.unit ?_, ha⟩) (quadraticChar_exists_neg_one hF)
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℤ)
⊢ IsUnit a
have contrapose : ∀ (ha : ¬IsUnit a), ¬Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
Tactic: contrapose ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
a : F
⊢ (↑((quadraticChar F : (a : F) → ℤ) a) : F) = a ^ (Fintype.card F / 2)
have pos : ∀ (ha : a = 0), (↑((quadraticChar F : (a : F) → ℤ) a) : F) = a ^ (Fintype.card F / 2)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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)
⊢ (↑((quadraticChar F : (a : F) → ℤ) a) : F) = a ^ (Fintype.card F / 2)
have neg : ∀ (ha : ¬a = 0), (↑((quadraticChar F : (a : F) → ℤ) a) : F) = a ^ (Fintype.card F / 2)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (hypothesis)
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
⊢ (↑((quadraticChar F : (a : F) → ℤ) a) : F) = a ^ (Fintype.card F / 2)
have this : 0 < Fintype.card F / 2
Tactic: have : 0 < Fintype.card F / 2 := Nat.div_pos Fintype.one_lt_card two_pos
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ (↑((quadraticChar F : (a : F) → ℤ) a) : F) = a ^ (Fintype.card F / 2)
have neg : (↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) : F) = a ^ (Fintype.card F / 2)
Tactic: rw [quadraticChar_eq_pow_of_char_ne_two hF ha]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ (↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) : F) = a ^ (Fintype.card F / 2)
have 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)
Tactic: by_cases ha' : a ^ (Fintype.card F / 2) = 1
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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)
⊢ (↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) : F) = a ^ (Fintype.card F / 2)
have 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)
Tactic: by_cases ha' : a ^ (Fintype.card F / 2) = 1
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (hypothesis)
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)
have ha'' : a ^ (Fintype.card F / 2) = -1
Tactic: have ha'' := Or.resolve_left (FiniteField.pow_dichotomy hF ha) ha'
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ (↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) : F) = a ^ (Fintype.card F / 2)
have neg : Eq.{u_1 + 1} (α := F) (-1) 1 → Eq.{u_1 + 1} (α := F) 1 (-1)
Tactic: simp only [ha'', Int.cast_ite, Int.cast_one, Int.cast_neg, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
      Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
have 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 : ℤ)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
      Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
have 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 : ℤ)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
      Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
have pos : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (0 : ℤ)
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℤ) (0 : ℤ)
have pos : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) 0 : ℤ) (0 : ℤ)
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
      Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
have neg : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ∨
  Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (-1 : ℤ)
Tactic: right
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
⊢ Ne (α := MulChar F ℤ) (quadraticChar F) 1
have rcases : ∀ (a : Fˣ) (ha : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑a : F) : ℤ) (-1 : ℤ)),
  Ne (α := MulChar F ℤ) (quadraticChar F) 1
Tactic: rcases quadraticChar_exists_neg_one' hF with ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
a : F
⊢ (↑(card.{u_1} (α := F) (Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a})) : ℤ) =
    HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
have 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 : ℤ)
Tactic: by_cases h₀ : a = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℤ)
⊢ (↑(card.{u_1} (α := F) (Set.toFinset {x : F | HPow.hPow (β := ℕ) x 2 = a})) : ℤ) =
    HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
have 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 : ℤ)
Tactic: by_cases h₀ : a = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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}
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
have pos : ∀ (h : IsSquare a), (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
Tactic: by_cases h : IsSquare a
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℤ)
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
have neg : ∀ (h : ¬IsSquare a), (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
Tactic: by_cases h : IsSquare a
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
have pos : (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) 1 1
Tactic: rw [(quadraticChar_one_iff_isSquare h₀).mpr h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) 1 1
have pos : ∀ (b : F) (h : a = b * b), (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) 1 1
Tactic: rcases h with ⟨b, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (hypothesis)
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
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) 1 1
have h₁ : ¬b = 0
Tactic: rw [h, mul_self_eq_zero] at h₀
Cleared hypotheses: h₀, h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
have h₁ : ∀ (a : F), a ∈ s ↔ a ∈ [b, -b].toFinset
Tactic: ext1
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ a_1 ∈ s ↔ a_1 ∈ [b, -b].toFinset
have h₁ : ∀ (h : a = HPow.hPow (β := ℕ) b 2) (a : F), a ∈ s ↔ a ∈ [b, -b].toFinset
Tactic: rw [← pow_two] at h
Cleared hypotheses: h, a_1
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ a_1 ∈ s ↔ a_1 ∈ [b, -b].toFinset
have h₁ : HPow.hPow (β := ℕ) a_1 2 = HPow.hPow (β := ℕ) b 2 ↔ a_1 = b ∨ a_1 = -b
Tactic: simp_rw [s, Set.toFinset_setOf, mem_filter_univ, h, List.toFinset_cons, List.toFinset_nil,
          insert_empty_eq, mem_insert, mem_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (hypothesis)
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) : ℤ) = HAdd.hAdd (α := ℤ) 1 1
have h₁ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) 1 1
have pos : #s = HAdd.hAdd (α := ℕ) 1 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ #s = HAdd.hAdd (α := ℕ) 1 1
have pos : card (α := F) (insert b (insert (-b) ∅)) = HAdd.hAdd (α := ℕ) 1 1
Tactic: rw [h₁, List.toFinset_cons, List.toFinset_cons, List.toFinset_nil]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ)
have neg : (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (-1) 1
Tactic: rw [quadraticChar_neg_one_iff_not_isSquare.mpr h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ (↑(#s) : ℤ) = HAdd.hAdd (α := ℤ) (-1) 1
have neg : ∀ (x : F), x ∉ s
Tactic: simp only [neg_add_cancel, Int.natCast_eq_zero, card_eq_zero, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (hypothesis)
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) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4) : ℤ)
have h : 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)
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-1) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4) : ℤ)
have rw : (if HPow.hPow (α := F) (-1) (Fintype.card F / 2) = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (Fintype.card F / 2)
Tactic: rw [h, χ₄_eq_neg_one_pow (FiniteField.odd_card_of_char_ne_two hF)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℤ)
⊢ (if HPow.hPow (α := F) (-1) (Fintype.card F / 2) = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (Fintype.card F / 2)
have generalize : ∀ (n : ℕ), (if HPow.hPow (α := F) (-1) n = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) n
Tactic: generalize Fintype.card F / 2 = n
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℕ
⊢ (if HPow.hPow (α := F) (-1) n = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) n
have inl : ∀ (h₂ : Even 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₂
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ (if HPow.hPow (α := F) (-1) n = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) n
have inr : ∀ (h₂ : Odd 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₂
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
⊢ IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
have pos : ∀ (hF : ringChar F = 2), IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
Tactic: by_cases hF : ringChar F = 2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
have neg : ∀ (hF : ¬ringChar F = 2), IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
Tactic: by_cases hF : ringChar F = 2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
⊢ IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
have pos : ¬Fintype.card F % 4 = 3
Tactic: simp only [FiniteField.isSquare_of_char_two hF, Ne, true_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
have h₁ : Fintype.card F % 2 = 1
Tactic: have h₁ := FiniteField.odd_card_of_char_ne_two hF
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
have 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
Tactic: rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (one_ne_zero' F)),
      quadraticChar_neg_one hF, χ₄_nat_eq_if_mod_four, h₁]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
⊢ IsSquare.{u_1} (α := F) (-1) ↔ Fintype.card F % 4 ≠ 3
have pos : ∀ (hF : ringChar F = 2), 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