[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
[PROOFSTEP]
by_cases hc : p = 2
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
[PROOFSTEP]
subst hc
[GOAL]
case pos
inst✝ : Fact (Nat.Prime 2)
x : (ZMod 2)ˣ
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (2 / 2) = 1
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton, exists_const]
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
[PROOFSTEP]
have h₀ := FiniteField.unit_isSquare_iff (by rwa [ringChar_zmod_n]) x
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ ringChar (ZMod p) ≠ 2
[PROOFSTEP]
rwa [ringChar_zmod_n]
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
[PROOFSTEP]
have hs : (∃ y : (ZMod p)ˣ, y ^ 2 = x) ↔ IsSquare x :=
  by
  rw [isSquare_iff_exists_sq x]
  simp_rw [eq_comm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ IsSquare x
[PROOFSTEP]
rw [isSquare_iff_exists_sq x]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ ∃ c, x = c ^ 2
[PROOFSTEP]
simp_rw [eq_comm]
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
hs : (∃ y, y ^ 2 = x) ↔ IsSquare x
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
[PROOFSTEP]
rw [hs]
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
hs : (∃ y, y ^ 2 = x) ↔ IsSquare x
⊢ IsSquare x ↔ x ^ (p / 2) = 1
[PROOFSTEP]
rwa [card p] at h₀ 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a ↔ a ^ (p / 2) = 1
[PROOFSTEP]
apply (iff_congr _ (by simp [Units.ext_iff])).mp (euler_criterion_units p (Units.mk0 a ha))
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ Units.mk0 a ha ^ (p / 2) = 1 ↔ a ^ (p / 2) = 1
[PROOFSTEP]
simp [Units.ext_iff]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, y ^ 2 = Units.mk0 a ha) ↔ IsSquare a
[PROOFSTEP]
simp only [Units.ext_iff, sq, Units.val_mk0, Units.val_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, ↑y * ↑y = a) ↔ IsSquare a
[PROOFSTEP]
constructor
[GOAL]
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, ↑y * ↑y = a) → IsSquare a
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mp.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
y : (ZMod p)ˣ
hy : ↑y * ↑y = a
⊢ IsSquare a
[PROOFSTEP]
exact ⟨y, hy.symm⟩
[GOAL]
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a → ∃ y, ↑y * ↑y = a
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
⊢ ∃ y_1, ↑y_1 * ↑y_1 = y * y
[PROOFSTEP]
have hy : y ≠ 0 := by
  rintro rfl
  simp [zero_pow, mul_zero, ne_eq, not_true] at ha 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
⊢ y ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
ha : 0 * 0 ≠ 0
⊢ False
[PROOFSTEP]
simp [zero_pow, mul_zero, ne_eq, not_true] at ha 
[GOAL]
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ y_1, ↑y_1 * ↑y_1 = y * y
[PROOFSTEP]
refine' ⟨Units.mk0 y hy, _⟩
[GOAL]
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy) = y * y
[PROOFSTEP]
simp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
[PROOFSTEP]
cases' Prime.eq_two_or_odd (@Fact.out p.Prime _) with hp2 hp_odd
[GOAL]
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp2 : p = 2
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
[PROOFSTEP]
subst p
[GOAL]
case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
ha : a ≠ 0
⊢ a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
[PROOFSTEP]
revert a ha
[GOAL]
case inl
inst✝ : Fact (Nat.Prime 2)
⊢ ∀ {a : ZMod 2}, a ≠ 0 → a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
[PROOFSTEP]
intro a
[GOAL]
case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
⊢ a ≠ 0 → a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
[PROOFSTEP]
fin_cases a
[GOAL]
case inl.head
inst✝ : Fact (Nat.Prime 2)
⊢ { val := 0, isLt := (_ : 0 < 1 + 1) } ≠ 0 →
    { val := 0, isLt := (_ : 0 < 1 + 1) } ^ (2 / 2) = 1 ∨ { val := 0, isLt := (_ : 0 < 1 + 1) } ^ (2 / 2) = -1
case inl.tail.head
inst✝ : Fact (Nat.Prime 2)
⊢ { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ≠ 0 →
    { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ^ (2 / 2) = 1 ∨
      { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ^ (2 / 2) = -1
[PROOFSTEP]
tauto
[GOAL]
case inl.tail.head
inst✝ : Fact (Nat.Prime 2)
⊢ { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ≠ 0 →
    { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ^ (2 / 2) = 1 ∨
      { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ^ (2 / 2) = -1
[PROOFSTEP]
simp
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
[PROOFSTEP]
rw [← mul_self_eq_one_iff, ← pow_add, ← two_mul, two_mul_odd_div_two hp_odd]
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p - 1) = 1
[PROOFSTEP]
exact pow_card_sub_one_eq_one ha
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
cases' eq_or_ne (ringChar (ZMod p)) 2 with hc hc
[GOAL]
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
by_cases ha : (a : ZMod p) = 0
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
rw [legendreSym, ha, quadraticChar_zero, zero_pow (Nat.div_pos (@Fact.out p.Prime).two_le (succ_pos 1))]
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑0 = 0
[PROOFSTEP]
norm_cast
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
have := (ringChar_zmod_n p).symm.trans hc
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬↑a = 0
this : p = 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
subst p
[GOAL]
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑(legendreSym 2 a) = ↑a ^ (2 / 2)
[PROOFSTEP]
rw [legendreSym, quadraticChar_eq_one_of_char_two hc ha]
[GOAL]
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑1 = ↑a ^ (2 / 2)
[PROOFSTEP]
revert ha
[GOAL]
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬↑a = 0 → ↑1 = ↑a ^ (2 / 2)
[PROOFSTEP]
push_cast
[GOAL]
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬↑a = 0 → 1 = ↑a ^ (2 / 2)
[PROOFSTEP]
generalize (a : ZMod 2) = b
[GOAL]
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
b : ZMod 2
⊢ ¬b = 0 → 1 = b ^ (2 / 2)
[PROOFSTEP]
fin_cases b
[GOAL]
case neg.head
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬{ val := 0, isLt := (_ : 0 < 1 + 1) } = 0 → 1 = { val := 0, isLt := (_ : 0 < 1 + 1) } ^ (2 / 2)
[PROOFSTEP]
tauto
[GOAL]
case neg.tail.head
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬{ val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } = 0 →
    1 = { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ^ (2 / 2)
[PROOFSTEP]
simp
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
convert quadraticChar_eq_pow_of_char_ne_two' hc (a : ZMod p)
[GOAL]
case h.e'_3.h.e'_6.h.e'_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ p = Fintype.card (ZMod p)
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_3.h.e'_6.h.e'_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ p = Fintype.card (ZMod p)
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.h.e'_6.h.e'_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ p = Fintype.card (ZMod p)
[PROOFSTEP]
exact (card p).symm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p 0 = 0
[PROOFSTEP]
rw [legendreSym, Int.cast_zero, MulChar.map_zero]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p 1 = 1
[PROOFSTEP]
rw [legendreSym, Int.cast_one, MulChar.map_one]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a b : ℤ
⊢ legendreSym p (a * b) = legendreSym p a * legendreSym p b
[PROOFSTEP]
simp [legendreSym, Int.cast_mul, map_mul, quadraticCharFun_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ legendreSym p (a ^ 2) = 1
[PROOFSTEP]
dsimp only [legendreSym]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ ↑(quadraticChar (ZMod p)) ↑(a ^ 2) = 1
[PROOFSTEP]
rw [Int.cast_pow]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ ↑(quadraticChar (ZMod p)) (↑a ^ 2) = 1
[PROOFSTEP]
exact quadraticChar_sq_one' ha
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = legendreSym p (a % ↑p)
[PROOFSTEP]
simp only [legendreSym, int_cast_mod]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ legendreSym p ↑a = 1 ↔ IsSquare ↑a
[PROOFSTEP]
rw [eq_one_iff]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ IsSquare ↑↑a ↔ IsSquare ↑a
case ha0 p : ℕ inst✝ : Fact (Nat.Prime p) a : ℕ ha0 : ↑a ≠ 0 ⊢ ↑↑a ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
case ha0
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ ↑↑a ≠ 0
[PROOFSTEP]
exact_mod_cast ha0
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ legendreSym p ↑a = -1 ↔ ¬IsSquare ↑a
[PROOFSTEP]
rw [eq_neg_one_iff]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ ¬IsSquare ↑↑a ↔ ¬IsSquare ↑a
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ legendreSym p a = 1
[PROOFSTEP]
apply_fun (· * y⁻¹ ^ 2) at hxy 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0 * y⁻¹ ^ 2
⊢ legendreSym p a = 1
[PROOFSTEP]
simp only [zero_mul] at hxy 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0
⊢ legendreSym p a = 1
[PROOFSTEP]
rw [(by ring : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = (x * y⁻¹) ^ 2 - a * (y * y⁻¹) ^ 2), mul_inv_cancel hy, one_pow, mul_one,
  sub_eq_zero, pow_two] at hxy 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0
⊢ (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = (x * y⁻¹) ^ 2 - ↑a * (y * y⁻¹) ^ 2
[PROOFSTEP]
ring
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : x * y⁻¹ * (x * y⁻¹) = ↑a
⊢ legendreSym p a = 1
[PROOFSTEP]
exact (eq_one_iff p ha).mpr ⟨x * y⁻¹, hxy.symm⟩
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ legendreSym p a = 1
[PROOFSTEP]
haveI hy : y ≠ 0 := by
  rintro rfl
  rw [zero_pow' 2 (by norm_num), mul_zero, sub_zero, pow_eq_zero_iff (by norm_num : 0 < 2)] at hxy 
  exact hx hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ y ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * 0 ^ 2 = 0
⊢ False
[PROOFSTEP]
rw [zero_pow' 2 (by norm_num), mul_zero, sub_zero, pow_eq_zero_iff (by norm_num : 0 < 2)] at hxy 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * 0 ^ 2 = 0
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x ^ 2 = 0
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x = 0
⊢ False
[PROOFSTEP]
exact hx hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
hy : y ≠ 0
⊢ legendreSym p a = 1
[PROOFSTEP]
exact eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ x = 0 ∧ y = 0
[PROOFSTEP]
have ha : (a : ZMod p) ≠ 0 := by
  intro hf
  rw [(eq_zero_iff p a).mpr hf] at h 
  exact Int.zero_ne_neg_of_ne zero_ne_one h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ ↑a ≠ 0
[PROOFSTEP]
intro hf
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
hf : ↑a = 0
⊢ False
[PROOFSTEP]
rw [(eq_zero_iff p a).mpr hf] at h 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 0 = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
hf : ↑a = 0
⊢ False
[PROOFSTEP]
exact Int.zero_ne_neg_of_ne zero_ne_one h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
⊢ x = 0 ∧ y = 0
[PROOFSTEP]
by_contra hf
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
⊢ False
[PROOFSTEP]
cases' imp_iff_or_not.mp (not_and'.mp hf) with hx hy
[GOAL]
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hx : ¬x = 0
⊢ False
[PROOFSTEP]
rw [eq_one_of_sq_sub_mul_sq_eq_zero' ha hx hxy, eq_neg_self_iff] at h 
[GOAL]
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 1 = 0
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hx : ¬x = 0
⊢ False
[PROOFSTEP]
exact one_ne_zero h
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hy : ¬y = 0
⊢ False
[PROOFSTEP]
rw [eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy, eq_neg_self_iff] at h 
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 1 = 0
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hy : ¬y = 0
⊢ False
[PROOFSTEP]
exact one_ne_zero h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑p ∣ x ^ 2 - a * y ^ 2
⊢ ↑p ∣ x ∧ ↑p ∣ y
[PROOFSTEP]
simp_rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd] at hxy ⊢
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑(x ^ 2 - a * y ^ 2) = 0
⊢ ↑x = 0 ∧ ↑y = 0
[PROOFSTEP]
push_cast at hxy 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑x ^ 2 - ↑a * ↑y ^ 2 = 0
⊢ ↑x = 0 ∧ ↑y = 0
[PROOFSTEP]
exact eq_zero_mod_of_eq_neg_one h hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p (-1) = ↑χ₄ ↑p
[PROOFSTEP]
simp only [legendreSym, card p, quadraticChar_neg_one ((ringChar_zmod_n p).substr hp), Int.cast_neg, Int.cast_one]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsSquare (-1) ↔ p % 4 ≠ 3
[PROOFSTEP]
rw [FiniteField.isSquare_neg_one_iff, card p]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : x ^ 2 = -y ^ 2
⊢ (x / y) ^ 2 = -1
[PROOFSTEP]
apply_fun fun z => z / y ^ 2 at hxy 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : x ^ 2 / y ^ 2 = -y ^ 2 / y ^ 2
⊢ (x / y) ^ 2 = -1
[PROOFSTEP]
rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy 
