[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p 2 = ↑χ₈ ↑p
[PROOFSTEP]
have : (2 : ZMod p) = (2 : ℤ) := by norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ 2 = ↑2
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : 2 = ↑2
⊢ legendreSym p 2 = ↑χ₈ ↑p
[PROOFSTEP]
rw [legendreSym, ← this, quadraticChar_two ((ringChar_zmod_n p).substr hp), card p]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p (-2) = ↑χ₈' ↑p
[PROOFSTEP]
have : (-2 : ZMod p) = (-2 : ℤ) := by norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ -2 = ↑(-2)
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : -2 = ↑(-2)
⊢ legendreSym p (-2) = ↑χ₈' ↑p
[PROOFSTEP]
rw [legendreSym, ← this, quadraticChar_neg_two ((ringChar_zmod_n p).substr hp), card p]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare 2 ↔ p % 8 = 1 ∨ p % 8 = 7
[PROOFSTEP]
rw [FiniteField.isSquare_two_iff, card p]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
[PROOFSTEP]
have h₁ := Prime.mod_two_eq_one_iff_ne_two.mpr hp
[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
[PROOFSTEP]
rw [← mod_mod_of_dvd p (by norm_num : 2 ∣ 8)] at h₁ 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ 2 ∣ 8
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
[PROOFSTEP]
have h₂ := mod_lt p (by norm_num : 0 < 8)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
⊢ 0 < 8
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
h₂ : p % 8 < 8
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
[PROOFSTEP]
revert h₂ h₁
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 % 2 = 1 → p % 8 < 8 → (p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7)
[PROOFSTEP]
generalize p % 8 = m
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
m : ℕ
⊢ m % 2 = 1 → m < 8 → (m ≠ 3 ∧ m ≠ 5 ↔ m = 1 ∨ m = 7)
[PROOFSTEP]
clear! p
[GOAL]
m : ℕ
⊢ m % 2 = 1 → m < 8 → (m ≠ 3 ∧ m ≠ 5 ↔ m = 1 ∨ m = 7)
[PROOFSTEP]
intros
[GOAL]
m : ℕ
h₁✝ : m % 2 = 1
h₂✝ : m < 8
⊢ m ≠ 3 ∧ m ≠ 5 ↔ m = 1 ∨ m = 7
[PROOFSTEP]
interval_cases m
[GOAL]
case «0»
m : ℕ
h₁✝ : 0 % 2 = 1
h₂✝ : 0 < 8
⊢ 0 ≠ 3 ∧ 0 ≠ 5 ↔ 0 = 1 ∨ 0 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «1»
m : ℕ
h₁✝ : 1 % 2 = 1
h₂✝ : 1 < 8
⊢ 1 ≠ 3 ∧ 1 ≠ 5 ↔ 1 = 1 ∨ 1 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «2»
m : ℕ
h₁✝ : 2 % 2 = 1
h₂✝ : 2 < 8
⊢ 2 ≠ 3 ∧ 2 ≠ 5 ↔ 2 = 1 ∨ 2 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «3»
m : ℕ
h₁✝ : 3 % 2 = 1
h₂✝ : 3 < 8
⊢ 3 ≠ 3 ∧ 3 ≠ 5 ↔ 3 = 1 ∨ 3 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «4»
m : ℕ
h₁✝ : 4 % 2 = 1
h₂✝ : 4 < 8
⊢ 4 ≠ 3 ∧ 4 ≠ 5 ↔ 4 = 1 ∨ 4 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «5»
m : ℕ
h₁✝ : 5 % 2 = 1
h₂✝ : 5 < 8
⊢ 5 ≠ 3 ∧ 5 ≠ 5 ↔ 5 = 1 ∨ 5 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «6»
m : ℕ
h₁✝ : 6 % 2 = 1
h₂✝ : 6 < 8
⊢ 6 ≠ 3 ∧ 6 ≠ 5 ↔ 6 = 1 ∨ 6 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «7»
m : ℕ
h₁✝ : 7 % 2 = 1
h₂✝ : 7 < 8
⊢ 7 ≠ 3 ∧ 7 ≠ 5 ↔ 7 = 1 ∨ 7 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare (-2) ↔ p % 8 = 1 ∨ p % 8 = 3
[PROOFSTEP]
rw [FiniteField.isSquare_neg_two_iff, card p]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
[PROOFSTEP]
have h₁ := Prime.mod_two_eq_one_iff_ne_two.mpr hp
[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
[PROOFSTEP]
rw [← mod_mod_of_dvd p (by norm_num : 2 ∣ 8)] at h₁ 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ 2 ∣ 8
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
[PROOFSTEP]
have h₂ := mod_lt p (by norm_num : 0 < 8)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
⊢ 0 < 8
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
h₂ : p % 8 < 8
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
[PROOFSTEP]
revert h₂ h₁
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 % 2 = 1 → p % 8 < 8 → (p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3)
[PROOFSTEP]
generalize p % 8 = m
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
m : ℕ
⊢ m % 2 = 1 → m < 8 → (m ≠ 5 ∧ m ≠ 7 ↔ m = 1 ∨ m = 3)
[PROOFSTEP]
clear! p
[GOAL]
m : ℕ
⊢ m % 2 = 1 → m < 8 → (m ≠ 5 ∧ m ≠ 7 ↔ m = 1 ∨ m = 3)
[PROOFSTEP]
intros
[GOAL]
m : ℕ
h₁✝ : m % 2 = 1
h₂✝ : m < 8
⊢ m ≠ 5 ∧ m ≠ 7 ↔ m = 1 ∨ m = 3
[PROOFSTEP]
interval_cases m
[GOAL]
case «0»
m : ℕ
h₁✝ : 0 % 2 = 1
h₂✝ : 0 < 8
⊢ 0 ≠ 5 ∧ 0 ≠ 7 ↔ 0 = 1 ∨ 0 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «1»
m : ℕ
h₁✝ : 1 % 2 = 1
h₂✝ : 1 < 8
⊢ 1 ≠ 5 ∧ 1 ≠ 7 ↔ 1 = 1 ∨ 1 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «2»
m : ℕ
h₁✝ : 2 % 2 = 1
h₂✝ : 2 < 8
⊢ 2 ≠ 5 ∧ 2 ≠ 7 ↔ 2 = 1 ∨ 2 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «3»
m : ℕ
h₁✝ : 3 % 2 = 1
h₂✝ : 3 < 8
⊢ 3 ≠ 5 ∧ 3 ≠ 7 ↔ 3 = 1 ∨ 3 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «4»
m : ℕ
h₁✝ : 4 % 2 = 1
h₂✝ : 4 < 8
⊢ 4 ≠ 5 ∧ 4 ≠ 7 ↔ 4 = 1 ∨ 4 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «5»
m : ℕ
h₁✝ : 5 % 2 = 1
h₂✝ : 5 < 8
⊢ 5 ≠ 5 ∧ 5 ≠ 7 ↔ 5 = 1 ∨ 5 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «6»
m : ℕ
h₁✝ : 6 % 2 = 1
h₂✝ : 6 < 8
⊢ 6 ≠ 5 ∧ 6 ≠ 7 ↔ 6 = 1 ∨ 6 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «7»
m : ℕ
h₁✝ : 7 % 2 = 1
h₂✝ : 7 < 8
⊢ 7 ≠ 5 ∧ 7 ≠ 7 ↔ 7 = 1 ∨ 7 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have hp₁ := (Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left hp
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have hq₁ := (Prime.eq_two_or_odd <| @Fact.out q.Prime _).resolve_left hq
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : 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 = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have hq₂ : ringChar (ZMod q) ≠ 2 := (ringChar_zmod_n q).substr hq
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : 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 = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have h := quadraticChar_odd_prime ((ringChar_zmod_n p).substr hp) hq ((ringChar_zmod_n p).substr hpq)
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : 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 :
  ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑(Fintype.card (ZMod p))) * ↑(Fintype.card (ZMod p)))
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
rw [card p] at h 
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : 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 : ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑p) * ↑p)
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have nc : ∀ n r : ℕ, ((n : ℤ) : ZMod r) = n := fun n r => by norm_cast
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : 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 : ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑p) * ↑p)
n r : ℕ
⊢ ↑↑n = ↑n
[PROOFSTEP]
norm_cast
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : 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 : ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have nc' : (((-1) ^ (p / 2) : ℤ) : ZMod q) = (-1) ^ (p / 2) := by norm_cast
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : 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 : ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
⊢ ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)
[PROOFSTEP]
norm_cast
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : 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 : ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
nc' : ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
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₁]
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
[PROOFSTEP]
cases' eq_or_ne p q with h h
[GOAL]
case inl
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p = q
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
[PROOFSTEP]
subst p
[GOAL]
case inl
q : ℕ
inst✝¹ : Fact (Nat.Prime q)
hq : q ≠ 2
inst✝ : Fact (Nat.Prime q)
hp : q ≠ 2
⊢ legendreSym q ↑q = (-1) ^ (q / 2 * (q / 2)) * legendreSym q ↑q
[PROOFSTEP]
rw [(eq_zero_iff q q).mpr (by exact_mod_cast nat_cast_self q), mul_zero]
[GOAL]
q : ℕ
inst✝¹ : Fact (Nat.Prime q)
hq : q ≠ 2
inst✝ : Fact (Nat.Prime q)
hp : q ≠ 2
⊢ ↑↑q = 0
[PROOFSTEP]
exact_mod_cast nat_cast_self q
[GOAL]
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
[PROOFSTEP]
have qr := congr_arg (· * legendreSym p q) (quadratic_reciprocity hp hq h)
[GOAL]
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr :
  (fun x => x * legendreSym p ↑q) (legendreSym q ↑p * legendreSym p ↑q) =
    (fun x => x * legendreSym p ↑q) ((-1) ^ (p / 2 * (q / 2)))
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
[PROOFSTEP]
have : ((q : ℤ) : ZMod p) ≠ 0 := by exact_mod_cast prime_ne_zero p q h
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr :
  (fun x => x * legendreSym p ↑q) (legendreSym q ↑p * legendreSym p ↑q) =
    (fun x => x * legendreSym p ↑q) ((-1) ^ (p / 2 * (q / 2)))
⊢ ↑↑q ≠ 0
[PROOFSTEP]
exact_mod_cast prime_ne_zero p q h
[GOAL]
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr :
  (fun x => x * legendreSym p ↑q) (legendreSym q ↑p * legendreSym p ↑q) =
    (fun x => x * legendreSym p ↑q) ((-1) ^ (p / 2 * (q / 2)))
this : ↑↑q ≠ 0
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
[PROOFSTEP]
simpa only [mul_assoc, ← pow_two, sq_one p this, mul_one] using qr
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 1
hq : q ≠ 2
⊢ legendreSym q ↑p = legendreSym p ↑q
[PROOFSTEP]
rw [quadratic_reciprocity' (Prime.mod_two_eq_one_iff_ne_two.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]
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
⊢ legendreSym q ↑p = -legendreSym p ↑q
[PROOFSTEP]
let nop := @neg_one_pow_div_two_of_three_mod_four
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ legendreSym q ↑p = -legendreSym p ↑q
[PROOFSTEP]
rw [quadratic_reciprocity', pow_mul, nop hp, nop hq, neg_one_mul]
[GOAL]
case hp
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ p ≠ 2
[PROOFSTEP]
rwa [← Prime.mod_two_eq_one_iff_ne_two, odd_of_mod_four_eq_three]
[GOAL]
case hq
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ q ≠ 2
[PROOFSTEP]
rwa [← Prime.mod_two_eq_one_iff_ne_two, odd_of_mod_four_eq_three]
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
⊢ IsSquare ↑q ↔ IsSquare ↑p
[PROOFSTEP]
cases' eq_or_ne p q with h h
[GOAL]
case inl
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p = q
⊢ IsSquare ↑q ↔ IsSquare ↑p
[PROOFSTEP]
subst p
[GOAL]
case inl
q : ℕ
inst✝¹ : Fact (Nat.Prime q)
hq1 : q ≠ 2
inst✝ : Fact (Nat.Prime q)
hp1 : q % 4 = 1
⊢ IsSquare ↑q ↔ IsSquare ↑q
[PROOFSTEP]
rfl
[GOAL]
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
⊢ IsSquare ↑q ↔ IsSquare ↑p
[PROOFSTEP]
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]
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp3 : p % 4 = 3
hq3 : q % 4 = 3
hpq : p ≠ q
⊢ IsSquare ↑q ↔ ¬IsSquare ↑p
[PROOFSTEP]
rw [← eq_one_iff' p (prime_ne_zero p q hpq), ← eq_neg_one_iff' q, quadratic_reciprocity_three_mod_four hp3 hq3, neg_inj]
