awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)) :
      ℤ)
⊢ 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 rwa : ∀
  (h :
    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)) :
        ℤ)),
  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: rwa [card p] 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
hF : ringChar F ≠ 2
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare.{u_1} (α := F) (↑p : F) ↔
    Ne (α := ℤ)
      ((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)) :
        ℤ)
      (-1 : ℤ)
have inl : ∀ [inst_3 : Fact (Nat.Prime (ringChar F))] (hp : ringChar F ≠ 2),
  IsSquare.{u_1} (α := F) (↑(ringChar F) : F) ↔
    Ne (α := ℤ)
      ((quadraticChar (ZMod (ringChar F)) : (a : ZMod (ringChar F)) → ℤ)
          (HMul.hMul (α := ZMod (ringChar F))
            (↑((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4)) : ZMod (ringChar F))
            (↑(Fintype.card F) : ZMod (ringChar F))) :
        ℤ)
      (-1 : ℤ)
Tactic: rcases eq_or_ne (ringChar F) p with rfl | hFp
Cleared hypotheses: p, inst_2, hp
-- 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
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : p ≠ 2
inl :
  ∀ [inst_3 : Fact (Nat.Prime (ringChar F))] (hp : ringChar F ≠ 2),
    IsSquare.{u_1} (α := F) (↑(ringChar F) : F) ↔
      Ne (α := ℤ)
        ((quadraticChar (ZMod (ringChar F)) : (a : ZMod (ringChar F)) → ℤ)
            (HMul.hMul (α := ZMod (ringChar F))
              (↑((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4)) : ZMod (ringChar F))
              (↑(Fintype.card F) : ZMod (ringChar F))) :
          ℤ)
        (-1 : ℤ)
⊢ IsSquare.{u_1} (α := F) (↑p : F) ↔
    Ne (α := ℤ)
      ((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)) :
        ℤ)
      (-1 : ℤ)
have inr : ∀ (hFp : ringChar F ≠ p),
  IsSquare.{u_1} (α := F) (↑p : F) ↔
    Ne (α := ℤ)
      ((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)) :
        ℤ)
      (-1 : ℤ)
Tactic: rcases eq_or_ne (ringChar F) p with rfl | hFp
-- 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
inst_2 : Fact (Nat.Prime (ringChar F))
hp : ringChar F ≠ 2
⊢ IsSquare.{u_1} (α := F) (↑(ringChar F) : F) ↔
    Ne (α := ℤ)
      ((quadraticChar (ZMod (ringChar F)) : (a : ZMod (ringChar F)) → ℤ)
          (HMul.hMul (α := ZMod (ringChar F))
            (↑((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4)) : ZMod (ringChar F))
            (↑(Fintype.card F) : ZMod (ringChar F))) :
        ℤ)
      (-1 : ℤ)
have inl : ∀ (q : ℕ+) (hq : Nat.Prime (ringChar F)) (hq' : Fintype.card F = ringChar F ^ (↑q : ℕ)),
  IsSquare.{u_1} (α := F) (↑(ringChar F) : F) ↔
    Ne (α := ℤ)
      ((quadraticChar (ZMod (ringChar F)) : (a : ZMod (ringChar F)) → ℤ)
          (HMul.hMul (α := ZMod (ringChar F))
            (↑((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4)) : ZMod (ringChar F))
            (↑(Fintype.card F) : ZMod (ringChar F))) :
        ℤ)
      (-1 : ℤ)
Tactic: obtain ⟨q, hq, hq'⟩ := FiniteField.card F (ringChar F)
-- 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
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F ≠ p
⊢ IsSquare.{u_1} (α := F) (↑p : F) ↔
    Ne (α := ℤ)
      ((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)) :
        ℤ)
      (-1 : ℤ)
have inr : ¬Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑p : F) : ℤ) (-1 : ℤ) ↔
  Ne (α := ℤ)
    ((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)) :
      ℤ)
    (-1 : ℤ)
Tactic: rwa [← Iff.not_left quadraticChar_neg_one_iff_not_isSquare, quadraticChar_odd_prime hF hp]
-- 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
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F ≠ p
inr :
  ¬Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (↑p : F) : ℤ) (-1 : ℤ) ↔
    Ne (α := ℤ)
      ((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)) :
        ℤ)
      (-1 : ℤ)
⊢ IsSquare.{u_1} (α := F) (↑p : F) ↔
    Ne (α := ℤ)
      ((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)) :
        ℤ)
      (-1 : ℤ)
have inr₁ : ¬Eq (α := ℤ)
      ((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)) :
        ℤ)
      (-1 : ℤ) ↔
  Ne (α := ℤ)
    ((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)) :
      ℤ)
    (-1 : ℤ)
Tactic: rwa [← Iff.not_left quadraticChar_neg_one_iff_not_isSquare, quadraticChar_odd_prime hF hp]
-- 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
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare.{u_1} (α := F) (↑p : F) ↔
    Ne (α := ℤ)
      ((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)) :
        ℤ)
      (-1 : ℤ)
have inl : ∀ [inst_3 : Fact (Nat.Prime (ringChar F))] (hp : ringChar F ≠ 2),
  IsSquare.{u_1} (α := F) (↑(ringChar F) : F) ↔
    Ne (α := ℤ)
      ((quadraticChar (ZMod (ringChar F)) : (a : ZMod (ringChar F)) → ℤ)
          (HMul.hMul (α := ZMod (ringChar F))
            (↑((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4)) : ZMod (ringChar F))
            (↑(Fintype.card F) : ZMod (ringChar F))) :
        ℤ)
      (-1 : ℤ)
Tactic: classical
  rcases eq_or_ne (ringChar F) p with rfl | hFp
  · obtain ⟨q, hq, hq'⟩ := FiniteField.card F (ringChar F)
    simp [hq']
  · rwa [← Iff.not_left quadraticChar_neg_one_iff_not_isSquare, quadraticChar_odd_prime hF hp]
Cleared hypotheses: p, inst_2, hp
-- 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
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : p ≠ 2
inl :
  ∀ [inst_3 : Fact (Nat.Prime (ringChar F))] (hp : ringChar F ≠ 2),
    IsSquare.{u_1} (α := F) (↑(ringChar F) : F) ↔
      Ne (α := ℤ)
        ((quadraticChar (ZMod (ringChar F)) : (a : ZMod (ringChar F)) → ℤ)
            (HMul.hMul (α := ZMod (ringChar F))
              (↑((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card F) : ZMod 4)) : ZMod (ringChar F))
              (↑(Fintype.card F) : ZMod (ringChar F))) :
          ℤ)
        (-1 : ℤ)
⊢ IsSquare.{u_1} (α := F) (↑p : F) ↔
    Ne (α := ℤ)
      ((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)) :
        ℤ)
      (-1 : ℤ)
have inr : ∀ (hFp : ringChar F ≠ p),
  IsSquare.{u_1} (α := F) (↑p : F) ↔
    Ne (α := ℤ)
      ((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)) :
        ℤ)
      (-1 : ℤ)
Tactic: classical
  rcases eq_or_ne (ringChar F) p with rfl | hFp
  · obtain ⟨q, hq, hq'⟩ := FiniteField.card F (ringChar F)
    simp [hq']
  · rwa [← Iff.not_left quadraticChar_neg_one_iff_not_isSquare, quadraticChar_odd_prime hF hp]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ Eq (α := ZMod p) 2 (↑2 : ZMod p)
have norm_cast : Eq (α := ZMod p) 2 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p 2 = (χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8)
have this : Eq (α := ZMod p) 2 (↑2 : ZMod p)
Tactic: have : (2 : ZMod p) = (2 : ℤ) := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
this : Eq (α := ZMod p) 2 (↑2 : ZMod p)
⊢ legendreSym p 2 = (χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8)
have rw : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑2 : ZMod p) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
Tactic: rw [legendreSym, ← this, quadraticChar_two ((ringChar_zmod_n p).substr hp), card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
this : Eq (α := ZMod p) 2 (↑2 : ZMod p)
rw :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑2 : ZMod p) : ℤ)
    ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
⊢ legendreSym p 2 = (χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8)
have rw₁ : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) 2 : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
Tactic: rw [legendreSym, ← this, quadraticChar_two ((ringChar_zmod_n p).substr hp), card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
this : Eq (α := ZMod p) 2 (↑2 : ZMod p)
rw :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑2 : ZMod p) : ℤ)
    ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
rw₁ : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) 2 : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
⊢ legendreSym p 2 = (χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8)
have rw₂ : Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card (ZMod p)) : ZMod 8) : ℤ)
  ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
Tactic: rw [legendreSym, ← this, quadraticChar_two ((ringChar_zmod_n p).substr hp), card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
this : Eq (α := ZMod p) 2 (↑2 : ZMod p)
rw :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑2 : ZMod p) : ℤ)
    ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
rw₁ : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) 2 : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
rw₂ :
  Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card (ZMod p)) : ZMod 8) : ℤ)
    ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
⊢ legendreSym p 2 = (χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8)
have rw₃ : Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
Tactic: rw [legendreSym, ← this, quadraticChar_two ((ringChar_zmod_n p).substr hp), card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ Eq (α := ZMod p) (-2) (↑(-2) : ZMod p)
have norm_cast : Eq (α := ZMod p) (↑(Int.negSucc 1) : ZMod p) (↑(Int.negSucc 1) : ZMod p)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p (-2) = (χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8)
have this : Eq (α := ZMod p) (-2) (↑(-2) : ZMod p)
Tactic: have : (-2 : ZMod p) = (-2 : ℤ) := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
this : Eq (α := ZMod p) (-2) (↑(-2) : ZMod p)
⊢ legendreSym p (-2) = (χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8)
have rw : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(-2) : ZMod p) : ℤ)
  ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
Tactic: rw [legendreSym, ← this, quadraticChar_neg_two ((ringChar_zmod_n p).substr hp), card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
this : Eq (α := ZMod p) (-2) (↑(-2) : ZMod p)
rw :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(-2) : ZMod p) : ℤ)
    ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
⊢ legendreSym p (-2) = (χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8)
have rw₁ : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (-2) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
Tactic: rw [legendreSym, ← this, quadraticChar_neg_two ((ringChar_zmod_n p).substr hp), card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
this : Eq (α := ZMod p) (-2) (↑(-2) : ZMod p)
rw :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(-2) : ZMod p) : ℤ)
    ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
rw₁ : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (-2) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
⊢ legendreSym p (-2) = (χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8)
have rw₂ : Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(Fintype.card (ZMod p)) : ZMod 8) : ℤ)
  ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
Tactic: rw [legendreSym, ← this, quadraticChar_neg_two ((ringChar_zmod_n p).substr hp), card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
this : Eq (α := ZMod p) (-2) (↑(-2) : ZMod p)
rw :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(-2) : ZMod p) : ℤ)
    ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
rw₁ : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (-2) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
rw₂ :
  Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(Fintype.card (ZMod p)) : ZMod 8) : ℤ)
    ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
⊢ legendreSym p (-2) = (χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8)
have rw₃ : Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
Tactic: rw [legendreSym, ← this, quadraticChar_neg_two ((ringChar_zmod_n p).substr hp), card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare (α := ZMod p) 2 ↔ p % 8 = 1 ∨ p % 8 = 7
have rw : p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
Tactic: rw [FiniteField.isSquare_two_iff, card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
have h₁ : p % 2 = 1
Tactic: have h₁ := (Prime.mod_two_eq_one_iff_ne_two Fact.out).mpr hp
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare (α := ZMod p) (-2) ↔ p % 8 = 1 ∨ p % 8 = 3
have rw : p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
Tactic: rw [FiniteField.isSquare_neg_two_iff, card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
have h₁ : p % 2 = 1
Tactic: have h₁ := (Prime.mod_two_eq_one_iff_ne_two Fact.out).mpr hp
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (hypothesis)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
⊢ legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
have hp₁ : p % 2 = 1
Tactic: have hp₁ := (Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left hp
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (hypothesis)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
⊢ legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
have hq₁ : q % 2 = 1
Tactic: have hq₁ := (Prime.eq_two_or_odd <| @Fact.out q.Prime _).resolve_left hq
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (hypothesis)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
⊢ legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
have hq₂ : ringChar (ZMod q) ≠ 2
Tactic: have hq₂ : ringChar (ZMod q) ≠ 2 := (ringChar_zmod_n q).substr hq
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (hypothesis)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
⊢ legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
have h : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ)
  ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
      (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card (ZMod p)) : ZMod 4)) : ZMod q)
        (↑(Fintype.card (ZMod p)) : ZMod q)) :
    ℤ)
Tactic: have h :=
    quadraticChar_odd_prime ((ringChar_zmod_n p).substr hp) hq ((ringChar_zmod_n p).substr hpq)
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (hypothesis)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ)
    ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
        (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑(Fintype.card (ZMod p)) : ZMod 4)) : ZMod q)
          (↑(Fintype.card (ZMod p)) : ZMod q)) :
      ℤ)
⊢ legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
have h₁ : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ)
  ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
      (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) (↑p : ZMod q)) :
    ℤ)
Tactic: rw [card p] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ)
    ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
        (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) (↑p : ZMod q)) :
      ℤ)
n r : ℕ
⊢ Eq (α := ZMod r) (↑(↑n : ℤ) : ZMod r) (↑n : ZMod r)
have norm_cast : Eq (α := ZMod r) (↑n : ZMod r) (↑n : ZMod r)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (hypothesis)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ)
    ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
        (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) (↑p : ZMod q)) :
      ℤ)
⊢ legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
have nc : ∀ (n r : ℕ), Eq (α := ZMod r) (↑(↑n : ℤ) : ZMod r) (↑n : ZMod r)
Tactic: have nc : ∀ n r : ℕ, ((n : ℤ) : ZMod r) = n := fun n r => by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ)
    ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
        (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) (↑p : ZMod q)) :
      ℤ)
nc : ∀ (n r : ℕ), Eq (α := ZMod r) (↑(↑n : ℤ) : ZMod r) (↑n : ZMod r)
⊢ (↑(HPow.hPow (α := ℤ) (-1) (p / 2)) : ZMod q) = HPow.hPow (α := ZMod q) (-1) (p / 2)
have norm_cast : Eq (α := ZMod q) (↑(Int.negSucc 0 ^ (p / 2)) : ZMod q) (↑(Int.negSucc 0 ^ (p / 2)) : ZMod q)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (hypothesis)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ)
    ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
        (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) (↑p : ZMod q)) :
      ℤ)
nc : ∀ (n r : ℕ), Eq (α := ZMod r) (↑(↑n : ℤ) : ZMod r) (↑n : ZMod r)
⊢ legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
have nc' : (↑(HPow.hPow (α := ℤ) (-1) (p / 2)) : ZMod q) = HPow.hPow (α := ZMod q) (-1) (p / 2)
Tactic: have nc' : (((-1) ^ (p / 2) : ℤ) : ZMod q) = (-1) ^ (p / 2) := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ)
    ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
        (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) (↑p : ZMod q)) :
      ℤ)
nc : ∀ (n r : ℕ), Eq (α := ZMod r) (↑(↑n : ℤ) : ZMod r) (↑n : ZMod r)
nc' : (↑(HPow.hPow (α := ℤ) (-1) (p / 2)) : ZMod q) = HPow.hPow (α := ZMod q) (-1) (p / 2)
⊢ legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
have rw : HMul.hMul (α := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ) (legendreSym p (↑q : ℤ)) =
  HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
Tactic: rw [legendreSym, legendreSym, nc, nc, h, map_mul, mul_rotate', mul_comm (p / 2), ← pow_two,
    quadraticChar_sq_one (prime_ne_zero q p hpq.symm), mul_one, pow_mul, χ₄_eq_neg_one_pow hp₁, nc',
    map_pow, quadraticChar_neg_one hq₂, card q, χ₄_eq_neg_one_pow hq₁]