Theorem: book.quadratic_reciprocity.lemma_of_Gauss (FormalBook/Chapter_05.lean)

State before:
p✝ : ℕ
h_p : p✝ ≠ 2
inst✝¹ : Fact p✝.Prime
p : ℕ
inst✝ : Fact p.Prime
a : ℤ
h_a : ↑a ≠ 0
r : ℤ → ℤ
h_r : ∀ (i : ℤ), (-↑p - 1) / 2 ≤ r i ∧ r i ≤ (↑p - 1) / 2
H : ∀ (i : ℤ), ↑(r i) = ↑a * ↑i
⊢ LocallyFiniteOrder ℤ
Tactic:
sorry
State after:
no goals

State before:
p✝ : ℕ
h_p : p✝ ≠ 2
inst✝¹ : Fact p✝.Prime
p : ℕ
inst✝ : Fact p.Prime
a : ℤ
h_a : ↑a ≠ 0
r : ℤ → ℤ
h_r : ∀ (i : ℤ), (-↑p - 1) / 2 ≤ r i ∧ r i ≤ (↑p - 1) / 2
H : ∀ (i : ℤ), ↑(r i) = ↑a * ↑i
⊢ let_fun this := sorryAx (LocallyFiniteOrder ℤ);
  legendre_sym p a = ↑(image r (Icc 1 ((↑p - 1) / 2)) ∩ Icc (-(↑p - 1) / 2) (-1)).card
Tactic:
sorry
State after:
no goals