awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rw :
  HMul.hMul (α := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ) (legendreSym p (↑q : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 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) : ℤ)
    ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
  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₁]
-- 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)
rw :
  HMul.hMul (α := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ) (legendreSym p (↑q : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₁ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 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) : ℤ)
    ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
  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₁]
-- 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)
rw :
  HMul.hMul (α := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ) (legendreSym p (↑q : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₁ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₂ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 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) : ℤ)
    ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ) =
  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₁]
-- 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)
rw :
  HMul.hMul (α := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ) (legendreSym p (↑q : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₁ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₂ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₃ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 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) : ℤ)
    ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
        (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) (↑p : ZMod 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₁]
-- 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)
rw :
  HMul.hMul (α := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ) (legendreSym p (↑q : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₁ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₂ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₃ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₄ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
          (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) (↑p : ZMod q)) :
        ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 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) : ℤ)
    (HMul.hMul (α := ℤ) (β := ℤ)
      ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) : ℤ)
      ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod 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₁]
-- 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)
rw :
  HMul.hMul (α := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ) (legendreSym p (↑q : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₁ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₂ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₃ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₄ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
          (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) (↑p : ZMod q)) :
        ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₅ :
  HMul.hMul (α := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      (HMul.hMul (α := ℤ) (β := ℤ)
        ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) : ℤ)
        ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
⊢ legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
have rw₆ : HMul.hMul (α := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) : ℤ)
    (HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod 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₁]
-- 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
⊢ legendreSym q (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ)
have inl : ∀ [inst_2 : Fact (Nat.Prime p)] (hq : p ≠ 2),
  legendreSym p (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (p / 2)) * legendreSym p (↑p : ℤ)
Tactic: rcases eq_or_ne p q with rfl | h
Cleared hypotheses: q, inst_1, hq
-- 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
inl :
  ∀ [inst_2 : Fact (Nat.Prime p)] (hq : p ≠ 2),
    legendreSym p (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (p / 2)) * legendreSym p (↑p : ℤ)
⊢ legendreSym q (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ)
have inr : ∀ (h : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
inst_1 : Fact (Nat.Prime p)
hq : p ≠ 2
⊢ legendreSym p (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (p / 2)) * legendreSym p (↑p : ℤ)
have inl : 0 = HPow.hPow (α := ℤ) (-1) (p / 2 * (p / 2)) * 0
Tactic: rw [(eq_zero_iff p p).mpr (mod_cast natCast_self p), mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
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
⊢ legendreSym p (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (p / 2)) * legendreSym p (↑p : ℤ)
have inl₁ : Eq (α := ℤ) 0 0
Tactic: rw [(eq_zero_iff p p).mpr (mod_cast natCast_self p), mul_zero]
-- 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
h : p ≠ q
⊢ legendreSym q (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ)
have 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))))
Tactic: have qr := congr_arg (· * legendreSym p q) (quadratic_reciprocity hp hq h)
-- 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
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))))
⊢ legendreSym q (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ)
have this : Ne (α := ZMod p) (↑(↑q : ℤ) : ZMod p) 0
Tactic: have : ((q : ℤ) : ZMod p) ≠ 0 := mod_cast prime_ne_zero p q 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 % 4 = 1
hq : q ≠ 2
⊢ legendreSym q (↑p : ℤ) = legendreSym p (↑q : ℤ)
have rw : HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ) = 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]
-- 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 % 4 = 1
hq : q ≠ 2
rw : HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ) = legendreSym p (↑q : ℤ)
⊢ legendreSym q (↑p : ℤ) = legendreSym p (↑q : ℤ)
have rw₁ : HPow.hPow (α := ℤ) (-1) (p / 2) ^ (q / 2) * legendreSym p (↑q : ℤ) = 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]
-- 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 % 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 : ℤ)
⊢ legendreSym q (↑p : ℤ) = legendreSym p (↑q : ℤ)
have rw₂ : HPow.hPow (α := ℤ) 1 (q / 2) * legendreSym p (↑q : ℤ) = 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]
-- 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 % 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 : ℤ)
⊢ legendreSym q (↑p : ℤ) = legendreSym p (↑q : ℤ)
have rw₃ : 1 * legendreSym p (↑q : ℤ) = 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]
-- 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 % 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 : ℤ)
⊢ legendreSym q (↑p : ℤ) = legendreSym p (↑q : ℤ)
have rw₄ : legendreSym p (↑q : ℤ) = 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]
-- 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 % 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
⊢ legendreSym q (↑p : ℤ) = -legendreSym p (↑q : ℤ)
have hp₁ : p ≠ 2
Tactic: rw [quadratic_reciprocity', pow_mul, nop hp, nop hq, neg_one_mul]
-- 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 % 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
⊢ legendreSym q (↑p : ℤ) = -legendreSym p (↑q : ℤ)
have hq₁ : q ≠ 2
Tactic: rw [quadratic_reciprocity', pow_mul, nop hp, nop hq, neg_one_mul]
-- 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 % 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
⊢ p ≠ 2
have hp₁ : p % 2 = 1
Tactic: rwa [← Prime.mod_two_eq_one_iff_ne_two Fact.out, odd_of_mod_four_eq_three]
-- 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 % 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 = 1
⊢ p ≠ 2
have hp₂ : Eq (α := ℕ) 1 1
Tactic: rwa [← Prime.mod_two_eq_one_iff_ne_two Fact.out, odd_of_mod_four_eq_three]
-- 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 % 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
⊢ q ≠ 2
have hq₁ : q % 2 = 1
Tactic: rwa [← Prime.mod_two_eq_one_iff_ne_two Fact.out, odd_of_mod_four_eq_three]
-- 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 % 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
hq₁ : q % 2 = 1
⊢ q ≠ 2
have hq₂ : Eq (α := ℕ) 1 1
Tactic: rwa [← Prime.mod_two_eq_one_iff_ne_two Fact.out, odd_of_mod_four_eq_three]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ IsSquare (α := ZMod q) (↑p : ZMod q)
have inl : ∀ [inst_2 : Fact (Nat.Prime p)] (hq1 : p ≠ 2),
  IsSquare (α := ZMod p) (↑p : ZMod p) ↔ IsSquare (α := ZMod p) (↑p : ZMod p)
Tactic: rcases eq_or_ne p q with rfl | h
Cleared hypotheses: q, inst_1, hq1
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
inl :
  ∀ [inst_2 : Fact (Nat.Prime p)] (hq1 : p ≠ 2),
    IsSquare (α := ZMod p) (↑p : ZMod p) ↔ IsSquare (α := ZMod p) (↑p : ZMod p)
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ IsSquare (α := ZMod q) (↑p : ZMod q)
have inr : ∀ (h : p ≠ q), IsSquare (α := ZMod p) (↑q : ZMod p) ↔ IsSquare (α := ZMod q) (↑p : ZMod q)
Tactic: rcases eq_or_ne p q with rfl | 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)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ IsSquare (α := ZMod q) (↑p : ZMod q)
have inr : legendreSym p (↑q : ℤ) = 1 ↔ IsSquare (α := ZMod q) (↑p : ZMod q)
Tactic: rw [← eq_one_iff' p (prime_ne_zero p q h), ← eq_one_iff' q (prime_ne_zero q p h.symm),
      quadratic_reciprocity_one_mod_four hp1 hq1]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
inr : legendreSym p (↑q : ℤ) = 1 ↔ IsSquare (α := ZMod q) (↑p : ZMod q)
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ IsSquare (α := ZMod q) (↑p : ZMod q)
have inr₁ : legendreSym p (↑q : ℤ) = 1 ↔ legendreSym q (↑p : ℤ) = 1
Tactic: rw [← eq_one_iff' p (prime_ne_zero p q h), ← eq_one_iff' q (prime_ne_zero q p h.symm),
      quadratic_reciprocity_one_mod_four hp1 hq1]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
inr : legendreSym p (↑q : ℤ) = 1 ↔ IsSquare (α := ZMod q) (↑p : ZMod q)
inr₁ : legendreSym p (↑q : ℤ) = 1 ↔ legendreSym q (↑p : ℤ) = 1
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ IsSquare (α := ZMod q) (↑p : ZMod q)
have inr₂ : legendreSym p (↑q : ℤ) = 1 ↔ legendreSym p (↑q : ℤ) = 1
Tactic: rw [← eq_one_iff' p (prime_ne_zero p q h), ← eq_one_iff' q (prime_ne_zero q p h.symm),
      quadratic_reciprocity_one_mod_four hp1 hq1]