[GOAL]
a : ℕ
⊢ jacobiSymNat a 0 = 1
[PROOFSTEP]
rw [jacobiSymNat, jacobiSym.zero_right]
[GOAL]
a : ℕ
⊢ jacobiSymNat a 1 = 1
[PROOFSTEP]
rw [jacobiSymNat, jacobiSym.one_right]
[GOAL]
b : ℕ
hb : Nat.beq (b / 2) 0 = false
⊢ jacobiSymNat 0 b = 0
[PROOFSTEP]
rw [jacobiSymNat, Nat.cast_zero, jacobiSym.zero_left ?_]
[GOAL]
b : ℕ
hb : Nat.beq (b / 2) 0 = false
⊢ 1 < b
[PROOFSTEP]
calc
  1 < 2 * 1 := by decide
  _ ≤ 2 * (b / 2) := (Nat.mul_le_mul_of_nonneg_left (Nat.succ_le.mpr (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb))))
  _ ≤ b := Nat.mul_div_le b 2
[GOAL]
b : ℕ
hb : Nat.beq (b / 2) 0 = false
⊢ 1 < 2 * 1
[PROOFSTEP]
decide
[GOAL]
b : ℕ
⊢ jacobiSymNat 1 b = 1
[PROOFSTEP]
rw [jacobiSymNat, Nat.cast_one, jacobiSym.one_left]
[GOAL]
p : ℕ
pp : Fact (Nat.Prime p)
a r : ℤ
hr : IsInt (jacobiSym a p) r
⊢ IsInt (legendreSym p a) r
[PROOFSTEP]
rwa [@jacobiSym.legendreSym.to_jacobiSym p pp a]
[GOAL]
a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : ↑b = b'
hab : a % b' = ab
h : ↑ab' = ab
hr : jacobiSymNat ab' b = r
⊢ jacobiSym a b = r
[PROOFSTEP]
rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]
[GOAL]
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rw [← hr, jacobiSymNat, jacobiSymNat, _root_.jacobiSym.mod_left a b, ← hab]
[GOAL]
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSym (↑a % ↑b) b = jacobiSym (↑(a % b)) b
[PROOFSTEP]
rfl
[GOAL]
a b : ℕ
hb₀ : Nat.beq (b / 2) 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
⊢ jacobiSymNat a b = 0
[PROOFSTEP]
refine'
  jacobiSym.eq_zero_iff.mpr
    ⟨ne_of_gt ((Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb₀)).trans_le (Nat.div_le_self b 2)), fun hf => _⟩
[GOAL]
a b : ℕ
hb₀ : Nat.beq (b / 2) 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd ↑a ↑b = 1
⊢ False
[PROOFSTEP]
have h : 2 ∣ a.gcd b := Nat.dvd_gcd (Nat.dvd_of_mod_eq_zero ha) (Nat.dvd_of_mod_eq_zero hb₁)
[GOAL]
a b : ℕ
hb₀ : Nat.beq (b / 2) 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd ↑a ↑b = 1
h : 2 ∣ Nat.gcd a b
⊢ False
[PROOFSTEP]
change 2 ∣ (a : ℤ).gcd b at h 
[GOAL]
a b : ℕ
hb₀ : Nat.beq (b / 2) 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd ↑a ↑b = 1
h : 2 ∣ Int.gcd ↑a ↑b
⊢ False
[PROOFSTEP]
rw [hf, ← even_iff_two_dvd] at h 
[GOAL]
a b : ℕ
hb₀ : Nat.beq (b / 2) 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd ↑a ↑b = 1
h : Even 1
⊢ False
[PROOFSTEP]
exact Nat.not_even_one h
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
have ha' : legendreSym 2 a = 1 := by simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ legendreSym 2 ↑a = 1
[PROOFSTEP]
simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rcases eq_or_ne c 0 with (rfl | hc')
[GOAL]
case inl
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
ha' : legendreSym 2 ↑a = 1
hc : b / 2 = 0
hr : jacobiSymNat a 0 = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rw [← hr, Nat.eq_zero_of_dvd_of_div_eq_zero (Nat.dvd_of_mod_eq_zero hb) hc]
[GOAL]
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
⊢ jacobiSymNat a b = r
[PROOFSTEP]
haveI : NeZero c :=
  ⟨hc'⟩
    -- for `jacobiSym.mul_right`
[GOAL]
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right, ←
  jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
have : ((2 : ℕ) : ℤ).gcd b = 1 := by
  rw [Int.coe_nat_gcd, ← Nat.mod_add_div b 2, hb, Nat.gcd_add_mul_left_right, Nat.gcd_one_right]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ Int.gcd ↑2 ↑b = 1
[PROOFSTEP]
rw [Int.coe_nat_gcd, ← Nat.mod_add_div b 2, hb, Nat.gcd_add_mul_left_right, Nat.gcd_one_right]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
this : Int.gcd ↑2 ↑b = 1
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rwa [← Nat.mod_add_div a 4, ha, hc, Nat.zero_add, (by decide : 4 = 2 ^ 2), jacobiSymNat, Nat.cast_mul, Nat.cast_pow,
  jacobiSym.mul_left, jacobiSym.sq_one' this, one_mul]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
this : Int.gcd ↑2 ↑b = 1
⊢ 4 = 2 ^ 2
[PROOFSTEP]
decide
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
have hb' : Odd b := by
  rw [← Nat.div_add_mod b 8, hb, Odd]
  use 4 * (b / 8); rw [← Nat.mul_assoc]; congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Odd b
[PROOFSTEP]
rw [← Nat.div_add_mod b 8, hb, Odd]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ∃ k, 8 * (b / 8) + 1 = 2 * k + 1
[PROOFSTEP]
use 4 * (b / 8)
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 1 = 2 * (4 * (b / 8)) + 1
[PROOFSTEP]
rw [← Nat.mul_assoc]
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 1 = 2 * 4 * (b / 8) + 1
[PROOFSTEP]
congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rw [jacobiSymNat, ← Nat.mod_add_div a 2, ha, hc, Nat.zero_add, Nat.cast_mul, jacobiSym.mul_left, Nat.cast_two,
  jacobiSym.at_two hb', ZMod.χ₈_nat_mod_eight, hb]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ ↑ZMod.χ₈ ↑1 * jacobiSym (↑c) b = r
[PROOFSTEP]
norm_num
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSym (↑c) b = r
[PROOFSTEP]
exact hr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
have hb' : Odd b := by
  rw [← Nat.div_add_mod b 8, hb, Odd]
  use 4 * (b / 8) + 3; rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]; congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Odd b
[PROOFSTEP]
rw [← Nat.div_add_mod b 8, hb, Odd]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ∃ k, 8 * (b / 8) + 7 = 2 * k + 1
[PROOFSTEP]
use 4 * (b / 8) + 3
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 7 = 2 * (4 * (b / 8) + 3) + 1
[PROOFSTEP]
rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 7 = 2 * 4 * (b / 8) + (2 * 3 + 1)
[PROOFSTEP]
congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rw [jacobiSymNat, ← Nat.mod_add_div a 2, ha, hc, Nat.zero_add, Nat.cast_mul, jacobiSym.mul_left, Nat.cast_two,
  jacobiSym.at_two hb', ZMod.χ₈_nat_mod_eight, hb, (by decide : ZMod.χ₈ (7 : ℕ) = 1)]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ ↑ZMod.χ₈ ↑7 = 1
[PROOFSTEP]
decide
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ 1 * jacobiSym (↑c) b = r
[PROOFSTEP]
norm_num
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSym (↑c) b = r
[PROOFSTEP]
exact hr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = -r
[PROOFSTEP]
have hb' : Odd b := by
  rw [← Nat.div_add_mod b 8, hb, Odd]
  use 4 * (b / 8) + 1; rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]; congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Odd b
[PROOFSTEP]
rw [← Nat.div_add_mod b 8, hb, Odd]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ∃ k, 8 * (b / 8) + 3 = 2 * k + 1
[PROOFSTEP]
use 4 * (b / 8) + 1
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 3 = 2 * (4 * (b / 8) + 1) + 1
[PROOFSTEP]
rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 3 = 2 * 4 * (b / 8) + (2 * 1 + 1)
[PROOFSTEP]
congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSymNat a b = -r
[PROOFSTEP]
rw [jacobiSymNat, ← Nat.mod_add_div a 2, ha, hc, Nat.zero_add, Nat.cast_mul, jacobiSym.mul_left, Nat.cast_two,
  jacobiSym.at_two hb', ZMod.χ₈_nat_mod_eight, hb, (by decide : ZMod.χ₈ (3 : ℕ) = -1)]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ ↑ZMod.χ₈ ↑3 = -1
[PROOFSTEP]
decide
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ -1 * jacobiSym (↑c) b = -r
[PROOFSTEP]
norm_num
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSym (↑c) b = r
[PROOFSTEP]
exact hr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = -r
[PROOFSTEP]
have hb' : Odd b := by
  rw [← Nat.div_add_mod b 8, hb, Odd]
  use 4 * (b / 8) + 2; rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]; congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Odd b
[PROOFSTEP]
rw [← Nat.div_add_mod b 8, hb, Odd]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ∃ k, 8 * (b / 8) + 5 = 2 * k + 1
[PROOFSTEP]
use 4 * (b / 8) + 2
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 5 = 2 * (4 * (b / 8) + 2) + 1
[PROOFSTEP]
rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 5 = 2 * 4 * (b / 8) + (2 * 2 + 1)
[PROOFSTEP]
congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSymNat a b = -r
[PROOFSTEP]
rw [jacobiSymNat, ← Nat.mod_add_div a 2, ha, hc, Nat.zero_add, Nat.cast_mul, jacobiSym.mul_left, Nat.cast_two,
  jacobiSym.at_two hb', ZMod.χ₈_nat_mod_eight, hb, (by decide : ZMod.χ₈ (5 : ℕ) = -1)]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ ↑ZMod.χ₈ ↑5 = -1
[PROOFSTEP]
decide
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ -1 * jacobiSym (↑c) b = -r
[PROOFSTEP]
norm_num
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSym (↑c) b = r
[PROOFSTEP]
exact hr
[GOAL]
a b : ℕ
r : ℤ
ha : a % 4 = 1
hb : b % 2 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_one_mod_four ha (Nat.odd_iff.mpr hb)]
[GOAL]
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 4 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rwa [jacobiSymNat, ← jacobiSym.quadratic_reciprocity_one_mod_four hb (Nat.odd_iff.mpr ha)]
[GOAL]
a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = -r
[PROOFSTEP]
rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_three_mod_four ha hb, neg_inj]
