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
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: 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
⊢ IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
have pos : ∀ (hF : ringChar F = 2), IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
Tactic: by_cases hF : ringChar F = 2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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
⊢ IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
have neg : ∀ (hF : ¬ringChar F = 2), IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
Tactic: by_cases hF : ringChar F = 2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
⊢ IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
have h : Fintype.card F % 2 = 0
Tactic: have h := FiniteField.even_card_of_char_two hF
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
have pos : Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
Tactic: simp only [FiniteField.isSquare_of_char_two hF, true_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
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.GaussSum (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) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
have 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
Tactic: rw [← quadraticChar_one_iff_isSquare (Ring.two_ne_zero hF), quadraticChar_two hF,
      χ₈_nat_eq_if_mod_eight]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
⊢ IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
have pos : ∀ (hF : ringChar F = 2), 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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
⊢ IsSquare.{u_1} (α := F) 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
have neg : ∀ (hF : ¬ringChar F = 2), 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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) : ℤ)
have rw : -2 = HMul.hMul (α := F) (-1) 2
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-2) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)
have rw₁ : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (HMul.hMul (α := F) (-1) 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)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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) : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-2) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)
have rw₂ : HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) (-1) : ℤ) ((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)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-2) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)
have 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) : ℤ)
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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) : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-2) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)
have 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) : ℤ)
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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) : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-2) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)
have 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) : ℤ)
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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) : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (-2) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8) : ℤ)
have 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) : ℤ)
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
⊢ IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
have pos : ∀ (hF : ringChar F = 2), IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
Tactic: by_cases hF : ringChar F = 2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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
⊢ IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
have neg : ∀ (hF : ¬ringChar F = 2), IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
Tactic: by_cases hF : ringChar F = 2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
⊢ IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
have h : Fintype.card F % 2 = 0
Tactic: have h := FiniteField.even_card_of_char_two hF
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
have pos : Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
Tactic: simp only [FiniteField.isSquare_of_char_two hF, true_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
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.GaussSum (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) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
have 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
Tactic: rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (Ring.two_ne_zero hF)),
      quadraticChar_neg_two hF, χ₈'_nat_eq_if_mod_eight]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
⊢ IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
have pos : ∀ (hF : ringChar F = 2), 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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
⊢ IsSquare.{u_1} (α := F) (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
have neg : ∀ (hF : ¬ringChar F = 2), 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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
have obtain : ∀ (a : Fˣ) (ha : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑a : F) : ℤ) (-1 : ℤ)), χ ≠ 1
Tactic: obtain ⟨a, ha⟩ := quadraticChar_exists_neg_one' hF
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
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
have refine : Ne.{u_2 + 1} (α := F') ((χ : (a : F) → F') (↑a : F) : F') (1 : F')
Tactic: refine ne_one_iff.mpr ⟨a, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (hypothesis)
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')
⊢ 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')) :
      ℤ)
have hχ₁ : χ ≠ 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'
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (hypothesis)
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
⊢ 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')) :
      ℤ)
have 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)
Tactic: have h := Char.card_pow_card hχ₁ ((quadraticChar_isQuadratic F).comp _) h hF'
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (hypothesis)
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 (α := ℤ) ((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')) :
      ℤ)
have 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')
Tactic: rw [← quadraticChar_eq_pow_of_char_ne_two' hF'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst_3 : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑p : F) : ℤ)
    ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ)
        (HMul.hMul (α := ZMod p) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4)) : ZMod p)
          (↑(Fintype.card F) : ZMod p)) :
      ℤ)
have rw : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑p : F) : ℤ)
  ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ)
      (HMul.hMul (α := ZMod p) (↑((quadraticChar F : (a : F) → ℤ) (-1)) : ZMod p) (↑(Fintype.card F) : ZMod p)) :
    ℤ)
Tactic: rw [← quadraticChar_neg_one hF]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst_3 : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑p : F) : ℤ)
    ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ)
        (HMul.hMul (α := ZMod p) (↑((quadraticChar F : (a : F) → ℤ) (-1)) : ZMod p) (↑(Fintype.card F) : ZMod p)) :
      ℤ)
have h : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑(Fintype.card (ZMod p)) : F) : ℤ)
  ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ)
      (HMul.hMul (α := ZMod p) (↑((quadraticChar F : (a : F) → ℤ) (-1)) : ZMod p) (↑(Fintype.card F) : ZMod p)) :
    ℤ)
Tactic: 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)