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

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

Premises used: quadraticChar_isQuadratic, MulChar.IsQuadratic.eq_of_eq_coe, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst_3 : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
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)) :
      ℤ)
⊢ 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)) :
      ℤ)

Tactic:
rw [← quadraticChar_neg_one hF]

Premises used: quadraticChar_neg_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst_3 : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ 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)
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
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)) :
      ℤ)
rwa rwa₁ rwa₂ 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)) :
        ℤ)
⊢ 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

Premises used: ZMod.card
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
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 : ℤ)
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 : ℤ)
⊢ 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

Premises used: ringChar, eq_or_ne, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
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
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 : ℤ)
⊢ 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)

Premises used: FiniteField.card, ringChar
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
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
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:
simp [hq']
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
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 : ℤ)
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 : ℤ)
inr₂ : ringChar F ≠ p
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 : ℤ)
inr₄ inr₅ inr₆ : 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:
rwa [← Iff.not_left quadraticChar_neg_one_iff_not_isSquare, quadraticChar_odd_prime hF hp]

Premises used: Iff.not_left, quadraticChar_odd_prime, quadraticChar_neg_one_iff_not_isSquare
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
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 : ℤ)
inr 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 : ℤ)
⊢ 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]

Premises used: FiniteField.card, Iff.not_left, ringChar, eq_or_ne, quadraticChar_neg_one_iff_not_isSquare, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ZMod p) 2 2
⊢ Eq (α := ZMod p) 2 (↑2 : ZMod p)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ Eq (α := ZMod p) 2 (↑2 : ZMod p)

Tactic:
have : (2 : ZMod p) = (2 : ℤ) := by norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
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) : ℤ)
rw₃ rw₄ : Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
⊢ legendreSym p 2 = (χ₈ : (a : ZMod 8) → ℤ) (↑p : ZMod 8)

Tactic:
rw [legendreSym, ← this, quadraticChar_two ((ringChar_zmod_n p).substr hp), card p]

Premises used: quadraticChar_two, legendreSym, Eq.substr, ZMod.ringChar_zmod_n, ZMod.card
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ZMod p) (↑(Int.negSucc 1) : ZMod p) (↑(Int.negSucc 1) : ZMod p)
⊢ Eq (α := ZMod p) (-2) (↑(-2) : ZMod p)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ Eq (α := ZMod p) (-2) (↑(-2) : ZMod p)

Tactic:
have : (-2 : ZMod p) = (-2 : ℤ) := by norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
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) : ℤ)
rw₃ rw₄ : Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8) : ℤ)
⊢ legendreSym p (-2) = (χ₈' : (a : ZMod 8) → ℤ) (↑p : ZMod 8)

Tactic:
rw [legendreSym, ← this, quadraticChar_neg_two ((ringChar_zmod_n p).substr hp), card p]

Premises used: legendreSym, quadraticChar_neg_two, Eq.substr, ZMod.ringChar_zmod_n, ZMod.card
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
rw : p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
⊢ IsSquare (α := ZMod p) 2 ↔ p % 8 = 1 ∨ p % 8 = 7

Tactic:
rw [FiniteField.isSquare_two_iff, card p]

Premises used: FiniteField.isSquare_two_iff, ZMod.card
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 2 = 1

Tactic:
have h₁ := (Prime.mod_two_eq_one_iff_ne_two Fact.out).mpr hp
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
rw : p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
⊢ IsSquare (α := ZMod p) (-2) ↔ p % 8 = 1 ∨ p % 8 = 3

Tactic:
rw [FiniteField.isSquare_neg_two_iff, card p]

Premises used: FiniteField.isSquare_neg_two_iff, ZMod.card
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
⊢ p % 2 = 1

Tactic:
have hp₁ := (Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left hp
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
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
⊢ q % 2 = 1

Tactic:
have hq₁ := (Prime.eq_two_or_odd <| @Fact.out q.Prime _).resolve_left hq
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
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
⊢ ringChar (ZMod q) ≠ 2

Tactic:
have hq₂ : ringChar (ZMod q) ≠ 2 := (ringChar_zmod_n q).substr hq
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
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
⊢ 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)
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
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)) :
      ℤ)
⊢ 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

Premises used: ZMod.card
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
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 : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ZMod r) (↑n : ZMod r) (↑n : ZMod r)
⊢ Eq (α := ZMod r) (↑(↑n : ℤ) : ZMod r) (↑n : ZMod r)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
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)

Tactic:
have nc : ∀ n r : ℕ, ((n : ℤ) : ZMod r) = n := fun n r => by norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
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)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq (α := ZMod q) (↑(Int.negSucc 0 ^ (p / 2)) : ZMod q) (↑(Int.negSucc 0 ^ (p / 2)) : ZMod q)
⊢ (↑(HPow.hPow (α := ℤ) (-1) (p / 2)) : ZMod q) = HPow.hPow (α := ZMod q) (-1) (p / 2)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
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)

Tactic:
have nc' : (((-1) ^ (p / 2) : ℤ) : ZMod q) = (-1) ^ (p / 2) := by norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
inl :
  ∀ [inst_2 : Fact (Nat.Prime p)] (hq : p ≠ 2),
    legendreSym p (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (p / 2)) * legendreSym p (↑p : ℤ)
inr : ∀ (h : p ≠ q), legendreSym q (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ)
⊢ legendreSym q (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ)

Tactic:
rcases eq_or_ne p q with rfl | h

Premises used: eq_or_ne, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
inst_1 : Fact (Nat.Prime p)
hq : p ≠ 2
inl : 0 = HPow.hPow (α := ℤ) (-1) (p / 2 * (p / 2)) * 0
inl₁ inl₂ : Eq (α := ℤ) 0 0
⊢ legendreSym p (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (p / 2)) * legendreSym p (↑p : ℤ)

Tactic:
rw [(eq_zero_iff p p).mpr (mod_cast natCast_self p), mul_zero]

Premises used: Iff.mpr, Int.cast, Int.cast_natCast, ZMod.natCast_self, congrArg, Int.cast_zero, cast, Nat.cast, MulZeroClass.mul_zero, legendreSym.eq_zero_iff, congr, Nat.cast_zero, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
⊢ Eq (α := ℤ) ((fun (x : ℤ) ↦ x * legendreSym p (↑q : ℤ)) (legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ)))
    ((fun (x : ℤ) ↦ x * legendreSym p (↑q : ℤ)) (HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))))

Tactic:
have qr := congr_arg (· * legendreSym p q) (quadratic_reciprocity hp hq h)
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr :
  Eq (α := ℤ) ((fun (x : ℤ) ↦ x * legendreSym p (↑q : ℤ)) (legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ)))
    ((fun (x : ℤ) ↦ x * legendreSym p (↑q : ℤ)) (HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))))
⊢ Ne (α := ZMod p) (↑(↑q : ℤ) : ZMod p) 0

Tactic:
have : ((q : ℤ) : ZMod p) ≠ 0 := mod_cast prime_ne_zero p q h
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr :
  Eq (α := ℤ) ((fun (x : ℤ) ↦ x * legendreSym p (↑q : ℤ)) (legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ)))
    ((fun (x : ℤ) ↦ x * legendreSym p (↑q : ℤ)) (HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))))
this : Ne (α := ZMod p) (↑(↑q : ℤ) : ZMod p) 0
⊢ legendreSym q (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ)

Tactic:
simpa only [mul_assoc, ← pow_two, sq_one p this, mul_one] using qr

Premises used: pow_two, legendreSym.sq_one, mul_assoc, mul_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p % 4 = 1
hq : q ≠ 2
rw : HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ) = legendreSym p (↑q : ℤ)
rw₁ : HPow.hPow (α := ℤ) (-1) (p / 2) ^ (q / 2) * legendreSym p (↑q : ℤ) = legendreSym p (↑q : ℤ)
rw₂ : HPow.hPow (α := ℤ) 1 (q / 2) * legendreSym p (↑q : ℤ) = legendreSym p (↑q : ℤ)
rw₃ : 1 * legendreSym p (↑q : ℤ) = legendreSym p (↑q : ℤ)
rw₄ rw₅ : legendreSym p (↑q : ℤ) = legendreSym p (↑q : ℤ)
⊢ legendreSym q (↑p : ℤ) = legendreSym p (↑q : ℤ)

Tactic:
rw [quadratic_reciprocity'
      ((Prime.mod_two_eq_one_iff_ne_two Fact.out).mp (odd_of_mod_four_eq_one hp)) hq,
    pow_mul, neg_one_pow_div_two_of_one_mod_four hp, one_pow, one_mul]

Premises used: one_pow, ZMod.neg_one_pow_div_two_of_one_mod_four, Nat.odd_of_mod_four_eq_one, Nat.Prime.mod_two_eq_one_iff_ne_two, pow_mul, legendreSym.quadratic_reciprocity', Iff.mp, one_mul, Fact.out
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ} (hn : n % 4 = 3), HPow.hPow (α := ℤ) (-1) (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
hp₁ : p ≠ 2
hq₁ : q ≠ 2
⊢ legendreSym q (↑p : ℤ) = -legendreSym p (↑q : ℤ)

Tactic:
rw [quadratic_reciprocity', pow_mul, nop hp, nop hq, neg_one_mul]

Premises used: neg_one_mul, pow_mul, legendreSym.quadratic_reciprocity'