[GOAL]
a : ℤ
⊢ J(a | 0) = 1
[PROOFSTEP]
simp only [jacobiSym, factors_zero, List.prod_nil, List.pmap]
[GOAL]
a : ℤ
⊢ J(a | 1) = 1
[PROOFSTEP]
simp only [jacobiSym, factors_one, List.prod_nil, List.pmap]
[GOAL]
p : ℕ
fp : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = J(a | p)
[PROOFSTEP]
simp only [jacobiSym, factors_prime fp.1, List.prod_cons, List.prod_nil, mul_one, List.pmap]
[GOAL]
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂)
[PROOFSTEP]
rw [jacobiSym, ((perm_factors_mul hb₁ hb₂).pmap _).prod_eq, List.pmap_append, List.prod_append]
[GOAL]
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ List.prod (List.pmap (fun p pp => legendreSym p a) (factors b₁) (_ : ∀ (a : ℕ), a ∈ factors b₁ → Nat.Prime a)) *
      List.prod (List.pmap (fun p pp => legendreSym p a) (factors b₂) (_ : ∀ (a : ℕ), a ∈ factors b₂ → Nat.Prime a)) =
    J(a | b₁) * J(a | b₂)
case h
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ (a : ℕ), a ∈ factors b₁ ++ factors b₂ → Nat.Prime a
case h a : ℤ b₁ b₂ : ℕ hb₁ : b₁ ≠ 0 hb₂ : b₂ ≠ 0 ⊢ ∀ (a : ℕ), a ∈ factors b₁ ++ factors b₂ → Nat.Prime a
[PROOFSTEP]
case h => exact fun p hp => (List.mem_append.mp hp).elim prime_of_mem_factors prime_of_mem_factors
[GOAL]
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ (a : ℕ), a ∈ factors b₁ ++ factors b₂ → Nat.Prime a
[PROOFSTEP]
case h => exact fun p hp => (List.mem_append.mp hp).elim prime_of_mem_factors prime_of_mem_factors
[GOAL]
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ (a : ℕ), a ∈ factors b₁ ++ factors b₂ → Nat.Prime a
[PROOFSTEP]
exact fun p hp => (List.mem_append.mp hp).elim prime_of_mem_factors prime_of_mem_factors
[GOAL]
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ List.prod (List.pmap (fun p pp => legendreSym p a) (factors b₁) (_ : ∀ (a : ℕ), a ∈ factors b₁ → Nat.Prime a)) *
      List.prod (List.pmap (fun p pp => legendreSym p a) (factors b₂) (_ : ∀ (a : ℕ), a ∈ factors b₂ → Nat.Prime a)) =
    J(a | b₁) * J(a | b₂)
[PROOFSTEP]
case _ => rfl
[GOAL]
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ List.prod (List.pmap (fun p pp => legendreSym p a) (factors b₁) (_ : ∀ (a : ℕ), a ∈ factors b₁ → Nat.Prime a)) *
      List.prod (List.pmap (fun p pp => legendreSym p a) (factors b₂) (_ : ∀ (a : ℕ), a ∈ factors b₂ → Nat.Prime a)) =
    J(a | b₁) * J(a | b₂)
[PROOFSTEP]
case _ => rfl
[GOAL]
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ List.prod (List.pmap (fun p pp => legendreSym p a) (factors b₁) (_ : ∀ (a : ℕ), a ∈ factors b₁ → Nat.Prime a)) *
      List.prod (List.pmap (fun p pp => legendreSym p a) (factors b₂) (_ : ∀ (a : ℕ), a ∈ factors b₂ → Nat.Prime a)) =
    J(a | b₁) * J(a | b₂)
[PROOFSTEP]
rfl
[GOAL]
a : ℤ
b : ℕ
⊢ {0, 1, -1} = ↑(MonoidHom.mrange ↑SignType.castHom)
[PROOFSTEP]
rw [Set.pair_comm]
[GOAL]
a : ℤ
b : ℕ
⊢ {0, -1, 1} = ↑(MonoidHom.mrange ↑SignType.castHom)
[PROOFSTEP]
exact (SignType.range_eq SignType.castHom).symm
[GOAL]
a : ℤ
b : ℕ
⊢ ∀ (x : ℤ),
    x ∈ List.pmap (fun p pp => legendreSym p a) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x) →
      x ∈
        Submonoid.copy (MonoidHom.mrange ↑SignType.castHom) {0, 1, -1}
          (_ : {0, 1, -1} = ↑(MonoidHom.mrange ↑SignType.castHom))
[PROOFSTEP]
intro _ ha'
[GOAL]
a : ℤ
b : ℕ
x✝ : ℤ
ha' : x✝ ∈ List.pmap (fun p pp => legendreSym p a) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x)
⊢ x✝ ∈
    Submonoid.copy (MonoidHom.mrange ↑SignType.castHom) {0, 1, -1}
      (_ : {0, 1, -1} = ↑(MonoidHom.mrange ↑SignType.castHom))
[PROOFSTEP]
rcases List.mem_pmap.mp ha' with ⟨p, hp, rfl⟩
[GOAL]
case intro.intro
a : ℤ
b p : ℕ
hp : p ∈ factors b
ha' : legendreSym p a ∈ List.pmap (fun p pp => legendreSym p a) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x)
⊢ legendreSym p a ∈
    Submonoid.copy (MonoidHom.mrange ↑SignType.castHom) {0, 1, -1}
      (_ : {0, 1, -1} = ↑(MonoidHom.mrange ↑SignType.castHom))
[PROOFSTEP]
haveI : Fact p.Prime := ⟨prime_of_mem_factors hp⟩
[GOAL]
case intro.intro
a : ℤ
b p : ℕ
hp : p ∈ factors b
ha' : legendreSym p a ∈ List.pmap (fun p pp => legendreSym p a) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x)
this : Fact (Nat.Prime p)
⊢ legendreSym p a ∈
    Submonoid.copy (MonoidHom.mrange ↑SignType.castHom) {0, 1, -1}
      (_ : {0, 1, -1} = ↑(MonoidHom.mrange ↑SignType.castHom))
[PROOFSTEP]
exact quadraticChar_isQuadratic (ZMod p) a
[GOAL]
b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp => legendreSym p 1) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x)
⊢ z = 1
[PROOFSTEP]
let ⟨p, hp, he⟩ := List.mem_pmap.1 hz
[GOAL]
b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp => legendreSym p 1) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x)
p : ℕ
hp : p ∈ factors b
he : legendreSym p 1 = z
⊢ z = 1
[PROOFSTEP]
letI : Fact p.Prime := ⟨prime_of_mem_factors hp⟩
[GOAL]
b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp => legendreSym p 1) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x)
p : ℕ
hp : p ∈ factors b
he : legendreSym p 1 = z
this : Fact (Nat.Prime p) := { out := prime_of_mem_factors hp }
⊢ z = 1
[PROOFSTEP]
rw [← he, legendreSym.at_one]
[GOAL]
a₁ a₂ : ℤ
b : ℕ
⊢ J(a₁ * a₂ | b) = J(a₁ | b) * J(a₂ | b)
[PROOFSTEP]
simp_rw [jacobiSym, List.pmap_eq_map_attach, legendreSym.mul _ _ _]
[GOAL]
a₁ a₂ : ℤ
b : ℕ
⊢ List.prod (List.map (fun x => legendreSym (↑x) a₁ * legendreSym (↑x) a₂) (List.attach (factors b))) =
    List.prod (List.map (fun x => legendreSym (↑x) a₁) (List.attach (factors b))) *
      List.prod (List.map (fun x => legendreSym (↑x) a₂) (List.attach (factors b)))
[PROOFSTEP]
exact
  List.prod_map_mul (α := ℤ) (l := (factors b).attach) (f := fun x ↦
    @legendreSym x { out := prime_of_mem_factors x.2 } a₁) (g := fun x ↦
    @legendreSym x { out := prime_of_mem_factors x.2 } a₂)
[GOAL]
a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ 0 ∈ List.pmap (fun p pp => legendreSym p a) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x) ↔
    Int.gcd a ↑b ≠ 1
[PROOFSTEP]
rw [List.mem_pmap, Int.gcd_eq_natAbs, Ne, Prime.not_coprime_iff_dvd]
  -- porting note: Initially, `and_assoc'` and `and_comm'` were used on line 164 but they have
        -- been deprecated so we replace them with `and_assoc` and `and_comm`
[GOAL]
a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1 h, legendreSym a_1 a = 0) ↔ ∃ p, Nat.Prime p ∧ p ∣ Int.natAbs a ∧ p ∣ Int.natAbs ↑b
[PROOFSTEP]
simp_rw [legendreSym.eq_zero_iff _ _, int_cast_zmod_eq_zero_iff_dvd, mem_factors (NeZero.ne b), ← Int.coe_nat_dvd_left,
  Int.coe_nat_dvd, exists_prop, and_assoc, and_comm]
[GOAL]
a : ℤ
b : ℕ
h : Int.gcd a ↑b = 1
⊢ J(a | b) ≠ 0
[PROOFSTEP]
cases' eq_zero_or_neZero b with hb
[GOAL]
case inl
a : ℤ
b : ℕ
h : Int.gcd a ↑b = 1
hb : b = 0
⊢ J(a | b) ≠ 0
[PROOFSTEP]
rw [hb, zero_right]
[GOAL]
case inl
a : ℤ
b : ℕ
h : Int.gcd a ↑b = 1
hb : b = 0
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
case inr
a : ℤ
b : ℕ
h : Int.gcd a ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
case inr
a : ℤ
b : ℕ
h✝ : NeZero b
h : J(a | b) = 0
⊢ Int.gcd a ↑b ≠ 1
[PROOFSTEP]
exact eq_zero_iff_not_coprime.1 h
[GOAL]
a : ℤ
b : ℕ
h : J(a | b) = 0
⊢ b ≠ 0 ∧ Int.gcd a ↑b ≠ 1
[PROOFSTEP]
cases' eq_or_ne b 0 with hb hb
[GOAL]
case inl
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b = 0
⊢ b ≠ 0 ∧ Int.gcd a ↑b ≠ 1
[PROOFSTEP]
rw [hb, zero_right] at h 
[GOAL]
case inl
a : ℤ
b : ℕ
h : 1 = 0
hb : b = 0
⊢ b ≠ 0 ∧ Int.gcd a ↑b ≠ 1
[PROOFSTEP]
cases h
[GOAL]
case inr
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b ≠ 0
⊢ b ≠ 0 ∧ Int.gcd a ↑b ≠ 1
[PROOFSTEP]
exact ⟨hb, mt jacobiSym.ne_zero <| Classical.not_not.2 h⟩
[GOAL]
a : ℤ
b : ℕ
x✝ : b ≠ 0 ∧ Int.gcd a ↑b ≠ 1
hb : b ≠ 0
h : Int.gcd a ↑b ≠ 1
⊢ J(a | b) = 0
[PROOFSTEP]
rw [← neZero_iff] at hb 
[GOAL]
a : ℤ
b : ℕ
x✝ : b ≠ 0 ∧ Int.gcd a ↑b ≠ 1
hb : NeZero b
h : Int.gcd a ↑b ≠ 1
⊢ J(a | b) = 0
[PROOFSTEP]
exact eq_zero_iff_not_coprime.2 h
[GOAL]
b : ℕ
hb : 1 < b
⊢ Int.gcd 0 ↑b ≠ 1
[PROOFSTEP]
rw [Int.gcd_zero_left, Int.natAbs_ofNat]
[GOAL]
b : ℕ
hb : 1 < b
⊢ b ≠ 1
[PROOFSTEP]
exact hb.ne'
[GOAL]
a : ℤ
e b : ℕ
⊢ J(a ^ zero | b) = J(a | b) ^ zero
[PROOFSTEP]
rw [_root_.pow_zero, _root_.pow_zero, one_left]
[GOAL]
a : ℤ
e b x✝ : ℕ
ih : J(a ^ x✝ | b) = J(a | b) ^ x✝
⊢ J(a ^ succ x✝ | b) = J(a | b) ^ succ x✝
[PROOFSTEP]
rw [_root_.pow_succ, _root_.pow_succ, mul_left, ih]
[GOAL]
a : ℤ
b e : ℕ
⊢ J(a | b ^ e) = J(a | b) ^ e
[PROOFSTEP]
induction' e with e ih
[GOAL]
case zero
a : ℤ
b : ℕ
⊢ J(a | b ^ zero) = J(a | b) ^ zero
[PROOFSTEP]
rw [Nat.pow_zero, _root_.pow_zero, one_right]
[GOAL]
case succ
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
⊢ J(a | b ^ succ e) = J(a | b) ^ succ e
[PROOFSTEP]
cases' eq_zero_or_neZero b with hb
[GOAL]
case succ.inl
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
⊢ J(a | b ^ succ e) = J(a | b) ^ succ e
[PROOFSTEP]
rw [hb, zero_pow (succ_pos e), zero_right, one_pow]
[GOAL]
case succ.inr
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h✝ : NeZero b
⊢ J(a | b ^ succ e) = J(a | b) ^ succ e
[PROOFSTEP]
rw [_root_.pow_succ, _root_.pow_succ, mul_right, ih]
[GOAL]
a : ℤ
b : ℕ
h : Int.gcd a ↑b = 1
⊢ J(a | b) ^ 2 = 1
[PROOFSTEP]
cases' eq_one_or_neg_one h with h₁ h₁
[GOAL]
case inl
a : ℤ
b : ℕ
h : Int.gcd a ↑b = 1
h₁ : J(a | b) = 1
⊢ J(a | b) ^ 2 = 1
[PROOFSTEP]
rw [h₁]
[GOAL]
case inr
a : ℤ
b : ℕ
h : Int.gcd a ↑b = 1
h₁ : J(a | b) = -1
⊢ J(a | b) ^ 2 = 1
[PROOFSTEP]
rw [h₁]
[GOAL]
case inl
a : ℤ
b : ℕ
h : Int.gcd a ↑b = 1
h₁ : J(a | b) = 1
⊢ 1 ^ 2 = 1
[PROOFSTEP]
rfl
[GOAL]
case inr
a : ℤ
b : ℕ
h : Int.gcd a ↑b = 1
h₁ : J(a | b) = -1
⊢ (-1) ^ 2 = 1
[PROOFSTEP]
rfl
[GOAL]
a : ℤ
b : ℕ
h : Int.gcd a ↑b = 1
⊢ J(a ^ 2 | b) = 1
[PROOFSTEP]
rw [pow_left, sq_one h]
[GOAL]
a : ℤ
b : ℕ
⊢ ∀ (a_1 : ℕ), a_1 ∈ factors b → ∀ (h₁ h₂ : Nat.Prime a_1), legendreSym a_1 a = legendreSym a_1 (a % ↑b)
[PROOFSTEP]
rintro p hp _ h₂
[GOAL]
a : ℤ
b p : ℕ
hp : p ∈ factors b
h₁✝ h₂ : Nat.Prime p
⊢ legendreSym p a = legendreSym p (a % ↑b)
[PROOFSTEP]
letI : Fact p.Prime := ⟨h₂⟩
[GOAL]
a : ℤ
b p : ℕ
hp : p ∈ factors b
h₁✝ h₂ : Nat.Prime p
this : Fact (Nat.Prime p) := { out := h₂ }
⊢ legendreSym p a = legendreSym p (a % ↑b)
[PROOFSTEP]
conv_rhs => rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.coe_nat_dvd.2 <| dvd_of_mem_factors hp), ← legendreSym.mod]
[GOAL]
a : ℤ
b p : ℕ
hp : p ∈ factors b
h₁✝ h₂ : Nat.Prime p
this : Fact (Nat.Prime p) := { out := h₂ }
| legendreSym p (a % ↑b)
[PROOFSTEP]
rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.coe_nat_dvd.2 <| dvd_of_mem_factors hp), ← legendreSym.mod]
[GOAL]
a : ℤ
b p : ℕ
hp : p ∈ factors b
h₁✝ h₂ : Nat.Prime p
this : Fact (Nat.Prime p) := { out := h₂ }
| legendreSym p (a % ↑b)
[PROOFSTEP]
rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.coe_nat_dvd.2 <| dvd_of_mem_factors hp), ← legendreSym.mod]
[GOAL]
a : ℤ
b p : ℕ
hp : p ∈ factors b
h₁✝ h₂ : Nat.Prime p
this : Fact (Nat.Prime p) := { out := h₂ }
| legendreSym p (a % ↑b)
[PROOFSTEP]
rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.coe_nat_dvd.2 <| dvd_of_mem_factors hp), ← legendreSym.mod]
[GOAL]
a₁ a₂ : ℤ
b : ℕ
h : a₁ % ↑b = a₂ % ↑b
⊢ J(a₁ | b) = J(a₂ | b)
[PROOFSTEP]
rw [mod_left, h, ← mod_left]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : J(a | p) = -1
x y : ℤ
hxy : ↑p ∣ x ^ 2 - a * y ^ 2
⊢ ↑p ∣ x ∧ ↑p ∣ y
[PROOFSTEP]
rw [← legendreSym.to_jacobiSym] at 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]
exact legendreSym.prime_dvd_of_eq_neg_one h hxy
[GOAL]
l : List ℤ
n : ℕ
⊢ J(List.prod l | n) = List.prod (List.map (fun a => J(a | n)) l)
[PROOFSTEP]
induction' l with n l' ih
[GOAL]
case nil
n : ℕ
⊢ J(List.prod [] | n) = List.prod (List.map (fun a => J(a | n)) [])
[PROOFSTEP]
simp only [List.prod_nil, List.map_nil, one_left]
[GOAL]
case cons
n✝ : ℕ
n : ℤ
l' : List ℤ
ih : J(List.prod l' | n✝) = List.prod (List.map (fun a => J(a | n✝)) l')
⊢ J(List.prod (n :: l') | n✝) = List.prod (List.map (fun a => J(a | n✝)) (n :: l'))
[PROOFSTEP]
rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]
[GOAL]
a : ℤ
l : List ℕ
hl : ∀ (n : ℕ), n ∈ l → n ≠ 0
⊢ J(a | List.prod l) = List.prod (List.map (fun n => J(a | n)) l)
[PROOFSTEP]
induction' l with n l' ih
[GOAL]
case nil
a : ℤ
l : List ℕ
hl✝ : ∀ (n : ℕ), n ∈ l → n ≠ 0
hl : ∀ (n : ℕ), n ∈ [] → n ≠ 0
⊢ J(a | List.prod []) = List.prod (List.map (fun n => J(a | n)) [])
[PROOFSTEP]
simp only [List.prod_nil, one_right, List.map_nil]
[GOAL]
case cons
a : ℤ
l : List ℕ
hl✝ : ∀ (n : ℕ), n ∈ l → n ≠ 0
n : ℕ
l' : List ℕ
ih : (∀ (n : ℕ), n ∈ l' → n ≠ 0) → J(a | List.prod l') = List.prod (List.map (fun n => J(a | n)) l')
hl : ∀ (n_1 : ℕ), n_1 ∈ n :: l' → n_1 ≠ 0
⊢ J(a | List.prod (n :: l')) = List.prod (List.map (fun n => J(a | n)) (n :: l'))
[PROOFSTEP]
have hn :=
  hl n
    (List.mem_cons_self n l')
      -- `n ≠ 0`
[GOAL]
case cons
a : ℤ
l : List ℕ
hl✝ : ∀ (n : ℕ), n ∈ l → n ≠ 0
n : ℕ
l' : List ℕ
ih : (∀ (n : ℕ), n ∈ l' → n ≠ 0) → J(a | List.prod l') = List.prod (List.map (fun n => J(a | n)) l')
hl : ∀ (n_1 : ℕ), n_1 ∈ n :: l' → n_1 ≠ 0
hn : n ≠ 0
⊢ J(a | List.prod (n :: l')) = List.prod (List.map (fun n => J(a | n)) (n :: l'))
[PROOFSTEP]
have hl' := List.prod_ne_zero fun hf => hl 0 (List.mem_cons_of_mem _ hf) rfl
[GOAL]
case cons
a : ℤ
l : List ℕ
hl✝ : ∀ (n : ℕ), n ∈ l → n ≠ 0
n : ℕ
l' : List ℕ
ih : (∀ (n : ℕ), n ∈ l' → n ≠ 0) → J(a | List.prod l') = List.prod (List.map (fun n => J(a | n)) l')
hl : ∀ (n_1 : ℕ), n_1 ∈ n :: l' → n_1 ≠ 0
hn : n ≠ 0
hl' : List.prod l' ≠ 0
⊢ J(a | List.prod (n :: l')) = List.prod (List.map (fun n => J(a | n)) (n :: l'))
[PROOFSTEP]
have h := fun m hm =>
  hl m
    (List.mem_cons_of_mem _ hm)
      -- `∀ (m : ℕ), m ∈ l' → m ≠ 0`
[GOAL]
case cons
a : ℤ
l : List ℕ
hl✝ : ∀ (n : ℕ), n ∈ l → n ≠ 0
n : ℕ
l' : List ℕ
ih : (∀ (n : ℕ), n ∈ l' → n ≠ 0) → J(a | List.prod l') = List.prod (List.map (fun n => J(a | n)) l')
hl : ∀ (n_1 : ℕ), n_1 ∈ n :: l' → n_1 ≠ 0
hn : n ≠ 0
hl' : List.prod l' ≠ 0
h : ∀ (m : ℕ), m ∈ l' → m ≠ 0
⊢ J(a | List.prod (n :: l')) = List.prod (List.map (fun n => J(a | n)) (n :: l'))
[PROOFSTEP]
rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]
[GOAL]
a : ℤ
n : ℕ
h : J(a | n) = -1
⊢ ∃ p x, p ∣ n ∧ J(a | p) = -1
[PROOFSTEP]
have hn₀ : n ≠ 0 := by
  rintro rfl
  rw [zero_right, eq_neg_self_iff] at h 
  exact one_ne_zero h
[GOAL]
a : ℤ
n : ℕ
h : J(a | n) = -1
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
a : ℤ
h : J(a | 0) = -1
⊢ False
[PROOFSTEP]
rw [zero_right, eq_neg_self_iff] at h 
[GOAL]
a : ℤ
h : 1 = 0
⊢ False
[PROOFSTEP]
exact one_ne_zero h
[GOAL]
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
⊢ ∃ p x, p ∣ n ∧ J(a | p) = -1
[PROOFSTEP]
have hf₀ : ∀ p ∈ n.factors, p ≠ 0 := fun p hp => (Nat.pos_of_mem_factors hp).ne.symm
[GOAL]
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
hf₀ : ∀ (p : ℕ), p ∈ factors n → p ≠ 0
⊢ ∃ p x, p ∣ n ∧ J(a | p) = -1
[PROOFSTEP]
rw [← Nat.prod_factors hn₀, list_prod_right hf₀] at h 
[GOAL]
a : ℤ
n : ℕ
h : List.prod (List.map (fun n => J(a | n)) (factors n)) = -1
hn₀ : n ≠ 0
hf₀ : ∀ (p : ℕ), p ∈ factors n → p ≠ 0
⊢ ∃ p x, p ∣ n ∧ J(a | p) = -1
[PROOFSTEP]
obtain ⟨p, hmem, hj⟩ := List.mem_map.mp (List.neg_one_mem_of_prod_eq_neg_one h)
[GOAL]
case intro.intro
a : ℤ
n : ℕ
h : List.prod (List.map (fun n => J(a | n)) (factors n)) = -1
hn₀ : n ≠ 0
hf₀ : ∀ (p : ℕ), p ∈ factors n → p ≠ 0
p : ℕ
hmem : p ∈ factors n
hj : J(a | p) = -1
⊢ ∃ p x, p ∣ n ∧ J(a | p) = -1
[PROOFSTEP]
exact ⟨p, Nat.prime_of_mem_factors hmem, Nat.dvd_of_mem_factors hmem, hj⟩
[GOAL]
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : ↑a = r * r
⊢ False
[PROOFSTEP]
rw [← r.coe_valMinAbs, ← Int.cast_mul, int_cast_eq_int_cast_iff', ← sq] at ha 
[GOAL]
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = valMinAbs r ^ 2 % ↑b
⊢ False
[PROOFSTEP]
apply (by norm_num : ¬(0 : ℤ) ≤ -1)
[GOAL]
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = valMinAbs r ^ 2 % ↑b
⊢ ¬0 ≤ -1
[PROOFSTEP]
norm_num
[GOAL]
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = valMinAbs r ^ 2 % ↑b
⊢ 0 ≤ -1
[PROOFSTEP]
rw [← h, mod_left, ha, ← mod_left, pow_left]
[GOAL]
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = valMinAbs r ^ 2 % ↑b
⊢ 0 ≤ J(valMinAbs r | b) ^ 2
[PROOFSTEP]
apply sq_nonneg
[GOAL]
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ J(a | p) = -1 ↔ ¬IsSquare ↑a
[PROOFSTEP]
rw [← legendreSym.to_jacobiSym]
[GOAL]
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p a = -1 ↔ ¬IsSquare ↑a
[PROOFSTEP]
exact legendreSym.eq_neg_one_iff p
[GOAL]
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : J(a | p) = 1
⊢ ¬¬IsSquare ↑a
[PROOFSTEP]
rw [← nonsquare_iff_jacobiSym_eq_neg_one, h]
[GOAL]
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : J(a | p) = 1
⊢ ¬1 = -1
[PROOFSTEP]
decide
[GOAL]
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = ↑χ ↑p
b : ℕ
hb : Odd b
⊢ J(a | b) = ↑χ ↑b
[PROOFSTEP]
conv_rhs => rw [← prod_factors hb.pos.ne', cast_list_prod, χ.map_list_prod]
[GOAL]
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = ↑χ ↑p
b : ℕ
hb : Odd b
| ↑χ ↑b
[PROOFSTEP]
rw [← prod_factors hb.pos.ne', cast_list_prod, χ.map_list_prod]
[GOAL]
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = ↑χ ↑p
b : ℕ
hb : Odd b
| ↑χ ↑b
[PROOFSTEP]
rw [← prod_factors hb.pos.ne', cast_list_prod, χ.map_list_prod]
[GOAL]
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = ↑χ ↑p
b : ℕ
hb : Odd b
| ↑χ ↑b
[PROOFSTEP]
rw [← prod_factors hb.pos.ne', cast_list_prod, χ.map_list_prod]
[GOAL]
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = ↑χ ↑p
b : ℕ
hb : Odd b
⊢ J(a | b) = List.prod (List.map (↑χ) (List.map Nat.cast (factors b)))
[PROOFSTEP]
rw [jacobiSym, List.map_map, ← List.pmap_eq_map Nat.Prime _ _ fun _ => prime_of_mem_factors]
[GOAL]
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = ↑χ ↑p
b : ℕ
hb : Odd b
⊢ List.prod (List.pmap (fun p pp => legendreSym p a) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x)) =
    List.prod (List.pmap (fun a x => (↑χ ∘ Nat.cast) a) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = ↑χ ↑p
b : ℕ
hb : Odd b
⊢ List.pmap (fun p pp => legendreSym p a) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x) =
    List.pmap (fun a x => (↑χ ∘ Nat.cast) a) (factors b) (_ : ∀ (x : ℕ), x ∈ factors b → Nat.Prime x)
[PROOFSTEP]
apply List.pmap_congr
[GOAL]
case e_a.h
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = ↑χ ↑p
b : ℕ
hb : Odd b
⊢ ∀ (a_1 : ℕ), a_1 ∈ factors b → ∀ (h₁ : Nat.Prime a_1), Nat.Prime a_1 → legendreSym a_1 a = (↑χ ∘ Nat.cast) a_1
[PROOFSTEP]
exact fun p h pp _ => hp p pp (hb.ne_two_of_dvd_nat <| dvd_of_mem_factors h)
[GOAL]
a : ℤ
b : ℕ
hb : Odd b
⊢ J(-a | b) = ↑χ₄ ↑b * J(a | b)
[PROOFSTEP]
rw [neg_eq_neg_one_mul, mul_left, at_neg_one hb]
[GOAL]
m n : ℕ
hm : Odd m
hn : Odd n
⊢ qrSign m n = (-1) ^ (m / 2 * (n / 2))
[PROOFSTEP]
rw [qrSign, pow_mul, ← χ₄_eq_neg_one_pow (odd_iff.mp hm)]
[GOAL]
m n : ℕ
hm : Odd m
hn : Odd n
⊢ J(↑χ₄ ↑m | n) = ↑χ₄ ↑m ^ (n / 2)
[PROOFSTEP]
cases' odd_mod_four_iff.mp (odd_iff.mp hm) with h h
[GOAL]
case inl
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 1
⊢ J(↑χ₄ ↑m | n) = ↑χ₄ ↑m ^ (n / 2)
[PROOFSTEP]
rw [χ₄_nat_one_mod_four h, jacobiSym.one_left, one_pow]
[GOAL]
case inr
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 3
⊢ J(↑χ₄ ↑m | n) = ↑χ₄ ↑m ^ (n / 2)
[PROOFSTEP]
rw [χ₄_nat_three_mod_four h, ← χ₄_eq_neg_one_pow (odd_iff.mp hn), jacobiSym.at_neg_one hn]
[GOAL]
m n : ℕ
hm : Odd m
hn : Odd n
⊢ qrSign m n ^ 2 = 1
[PROOFSTEP]
rw [neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
[GOAL]
m₁ m₂ n : ℕ
⊢ qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n
[PROOFSTEP]
simp_rw [qrSign, Nat.cast_mul, map_mul, jacobiSym.mul_left]
[GOAL]
m n : ℕ
hm : Odd m
hn : Odd n
⊢ qrSign m n = qrSign n m
[PROOFSTEP]
rw [neg_one_pow hm hn, neg_one_pow hn hm, mul_comm (m / 2)]
[GOAL]
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
⊢ qrSign m n * x = y ↔ x = qrSign m n * y
[PROOFSTEP]
refine'
  ⟨fun h' =>
    let h := h'.symm
    _,
    fun h => _⟩
[GOAL]
case refine'_1
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := Eq.symm h'
⊢ x = qrSign m n * y
[PROOFSTEP]
rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
[GOAL]
case refine'_2
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
⊢ qrSign m n * x = y
[PROOFSTEP]
rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
[GOAL]
a b : ℕ
ha : Odd a
hb : Odd b
⊢ J(↑a | b) = qrSign b a * J(↑b | a)
[PROOFSTEP]
let rhs : ℕ → ℕ →* ℤ := fun a =>
  { toFun := fun x => qrSign x a * J(x | a)
    map_one' := by convert ← mul_one (M := ℤ) _; symm; all_goals apply one_left
    map_mul' := fun x y => by
      -- porting note: `simp_rw` on line 423 replaces `rw` to allow the rewrite rules to be
              -- applied under the binder `fun ↦ ...`simp_rw [qrSign.mul_left x y a, Nat.cast_mul, mul_left,
        mul_mul_mul_comm] }
[GOAL]
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a : ℕ
⊢ (fun x => qrSign x a * J(↑x | a)) 1 = 1
[PROOFSTEP]
convert ← mul_one (M := ℤ) _
[GOAL]
case h.e'_2.h.e'_6
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a : ℕ
⊢ 1 = J(↑1 | a)
case h.e'_3 a✝ b : ℕ ha : Odd a✝ hb : Odd b a : ℕ ⊢ qrSign 1 a = 1
[PROOFSTEP]
symm
[GOAL]
case h.e'_2.h.e'_6
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a : ℕ
⊢ J(↑1 | a) = 1
case h.e'_3 a✝ b : ℕ ha : Odd a✝ hb : Odd b a : ℕ ⊢ qrSign 1 a = 1
[PROOFSTEP]
all_goals apply one_left
[GOAL]
case h.e'_2.h.e'_6
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a : ℕ
⊢ J(↑1 | a) = 1
[PROOFSTEP]
apply one_left
[GOAL]
case h.e'_3
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a : ℕ
⊢ qrSign 1 a = 1
[PROOFSTEP]
apply one_left
[GOAL]
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a x y : ℕ
⊢ OneHom.toFun { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
      (x * y) =
    OneHom.toFun { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) } y
[PROOFSTEP]
simp_rw [qrSign.mul_left x y a, Nat.cast_mul, mul_left, mul_mul_mul_comm]
[GOAL]
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ :=
  fun a =>
    {
      toOneHom :=
        { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) },
      map_mul' :=
        (_ :
          ∀ (x y : ℕ),
            OneHom.toFun
                { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                (x * y) =
              OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  x *
                OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  y) }
⊢ J(↑a | b) = qrSign b a * J(↑b | a)
[PROOFSTEP]
have rhs_apply : ∀ a b : ℕ, rhs a b = qrSign b a * J(b | a) := fun a b => rfl
[GOAL]
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ :=
  fun a =>
    {
      toOneHom :=
        { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) },
      map_mul' :=
        (_ :
          ∀ (x y : ℕ),
            OneHom.toFun
                { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                (x * y) =
              OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  x *
                OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  y) }
rhs_apply : ∀ (a b : ℕ), ↑(rhs a) b = qrSign b a * J(↑b | a)
⊢ J(↑a | b) = qrSign b a * J(↑b | a)
[PROOFSTEP]
refine' value_at a (rhs a) (fun p pp hp => Eq.symm _) hb
[GOAL]
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ :=
  fun a =>
    {
      toOneHom :=
        { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) },
      map_mul' :=
        (_ :
          ∀ (x y : ℕ),
            OneHom.toFun
                { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                (x * y) =
              OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  x *
                OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  y) }
rhs_apply : ∀ (a b : ℕ), ↑(rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
⊢ ↑(rhs a) ↑p = legendreSym p ↑a
[PROOFSTEP]
have hpo := pp.eq_two_or_odd'.resolve_left hp
[GOAL]
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ :=
  fun a =>
    {
      toOneHom :=
        { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) },
      map_mul' :=
        (_ :
          ∀ (x y : ℕ),
            OneHom.toFun
                { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                (x * y) =
              OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  x *
                OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  y) }
rhs_apply : ∀ (a b : ℕ), ↑(rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ ↑(rhs a) ↑p = legendreSym p ↑a
[PROOFSTEP]
rw [@legendreSym.to_jacobiSym p ⟨pp⟩, rhs_apply, Nat.cast_id, qrSign.eq_iff_eq hpo ha, qrSign.symm hpo ha]
[GOAL]
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ :=
  fun a =>
    {
      toOneHom :=
        { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) },
      map_mul' :=
        (_ :
          ∀ (x y : ℕ),
            OneHom.toFun
                { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                (x * y) =
              OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  x *
                OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  y) }
rhs_apply : ∀ (a b : ℕ), ↑(rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ J(↑p | a) = qrSign a p * J(↑a | p)
[PROOFSTEP]
refine' value_at p (rhs p) (fun q pq hq => _) ha
[GOAL]
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ :=
  fun a =>
    {
      toOneHom :=
        { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) },
      map_mul' :=
        (_ :
          ∀ (x y : ℕ),
            OneHom.toFun
                { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                (x * y) =
              OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  x *
                OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  y) }
rhs_apply : ∀ (a b : ℕ), ↑(rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
⊢ legendreSym q ↑p = ↑(rhs p) ↑q
[PROOFSTEP]
have hqo := pq.eq_two_or_odd'.resolve_left hq
[GOAL]
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ :=
  fun a =>
    {
      toOneHom :=
        { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) },
      map_mul' :=
        (_ :
          ∀ (x y : ℕ),
            OneHom.toFun
                { toFun := fun x => qrSign x a * J(↑x | a), map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                (x * y) =
              OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  x *
                OneHom.toFun
                  { toFun := fun x => qrSign x a * J(↑x | a),
                    map_one' := (_ : (fun x => qrSign x a * J(↑x | a)) 1 = 1) }
                  y) }
rhs_apply : ∀ (a b : ℕ), ↑(rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
hqo : Odd q
⊢ legendreSym q ↑p = ↑(rhs p) ↑q
[PROOFSTEP]
rw [rhs_apply, Nat.cast_id, ← @legendreSym.to_jacobiSym p ⟨pp⟩, qrSign.symm hqo hpo, qrSign.neg_one_pow hpo hqo,
  @legendreSym.quadratic_reciprocity' p q ⟨pp⟩ ⟨pq⟩ hp hq]
[GOAL]
a b : ℕ
ha : Odd a
hb : Odd b
⊢ J(↑a | b) = (-1) ^ (a / 2 * (b / 2)) * J(↑b | a)
[PROOFSTEP]
rw [← qrSign.neg_one_pow ha hb, qrSign.symm ha hb, quadratic_reciprocity' ha hb]
[GOAL]
a b : ℕ
ha : a % 4 = 1
hb : Odd b
⊢ J(↑a | b) = J(↑b | a)
[PROOFSTEP]
rw [quadratic_reciprocity (odd_iff.mpr (odd_of_mod_four_eq_one ha)) hb, pow_mul, neg_one_pow_div_two_of_one_mod_four ha,
  one_pow, one_mul]
[GOAL]
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
⊢ J(↑a | b) = -J(↑b | a)
[PROOFSTEP]
let nop := @neg_one_pow_div_two_of_three_mod_four
[GOAL]
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ J(↑a | b) = -J(↑b | a)
[PROOFSTEP]
rw [quadratic_reciprocity, pow_mul, nop ha, nop hb, neg_one_mul]
[GOAL]
case ha
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ Odd a
[PROOFSTEP]
rwa [odd_iff, odd_of_mod_four_eq_three]
[GOAL]
case hb
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ Odd b
[PROOFSTEP]
rwa [odd_iff, odd_of_mod_four_eq_three]
[GOAL]
a b : ℕ
hb : Odd b
⊢ J(↑a | b) = J(↑a | b % (4 * a))
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha₀)
[GOAL]
case inl
b : ℕ
hb : Odd b
⊢ J(↑0 | b) = J(↑0 | b % (4 * 0))
[PROOFSTEP]
rw [mul_zero, mod_zero]
[GOAL]
case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
⊢ J(↑a | b) = J(↑a | b % (4 * a))
[PROOFSTEP]
have hb' : Odd (b % (4 * a)) := hb.mod_even (Even.mul_right (by norm_num) _)
[GOAL]
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
⊢ Even 4
[PROOFSTEP]
norm_num
[GOAL]
case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
⊢ J(↑a | b) = J(↑a | b % (4 * a))
[PROOFSTEP]
rcases exists_eq_pow_mul_and_not_dvd ha₀ 2 (by norm_num) with ⟨e, a', ha₁', ha₂⟩
[GOAL]
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
⊢ 2 ≠ 1
[PROOFSTEP]
norm_num
[GOAL]
case inr.intro.intro.intro
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
⊢ J(↑a | b) = J(↑a | b % (4 * a))
[PROOFSTEP]
have ha₁ := odd_iff.mpr (two_dvd_ne_zero.mp ha₁')
[GOAL]
case inr.intro.intro.intro
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑a | b) = J(↑a | b % (4 * a))
[PROOFSTEP]
nth_rw 2 [ha₂]
[GOAL]
case inr.intro.intro.intro
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑a | b) = J(↑(2 ^ e * a') | b % (4 * a))
[PROOFSTEP]
nth_rw 1 [ha₂]
[GOAL]
case inr.intro.intro.intro
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑(2 ^ e * a') | b) = J(↑(2 ^ e * a') | b % (4 * a))
[PROOFSTEP]
rw [Nat.cast_mul, mul_left, mul_left, quadratic_reciprocity' ha₁ hb, quadratic_reciprocity' ha₁ hb', Nat.cast_pow,
  pow_left, pow_left, Nat.cast_two, at_two hb, at_two hb']
[GOAL]
case inr.intro.intro.intro
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ ↑χ₈ ↑b ^ e * (qrSign b a' * J(↑b | a')) = ↑χ₈ ↑(b % (4 * a)) ^ e * (qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a'))
[PROOFSTEP]
congr 1
[GOAL]
case inr.intro.intro.intro.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ ↑χ₈ ↑b ^ e = ↑χ₈ ↑(b % (4 * a)) ^ e
case inr.intro.intro.intro.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ qrSign b a' * J(↑b | a') = qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a')
[PROOFSTEP]
swap
[GOAL]
case inr.intro.intro.intro.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ qrSign b a' * J(↑b | a') = qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a')
case inr.intro.intro.intro.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ ↑χ₈ ↑b ^ e = ↑χ₈ ↑(b % (4 * a)) ^ e
[PROOFSTEP]
congr 1
[GOAL]
case inr.intro.intro.intro.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ qrSign b a' = qrSign (b % (4 * a)) a'
[PROOFSTEP]
simp_rw [qrSign]
[GOAL]
case inr.intro.intro.intro.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑χ₄ ↑b | a') = J(↑χ₄ ↑(b % (4 * a)) | a')
[PROOFSTEP]
rw [χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * a)), mod_mod_of_dvd b (dvd_mul_right 4 a)]
[GOAL]
case inr.intro.intro.intro.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑b | a') = J(↑(b % (4 * a)) | a')
[PROOFSTEP]
rw [mod_left ↑(b % _), mod_left b, Int.coe_nat_mod, Int.emod_emod_of_dvd b]
[GOAL]
case inr.intro.intro.intro.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ ↑a' ∣ ↑(4 * a)
[PROOFSTEP]
simp only [ha₂, Nat.cast_mul, ← mul_assoc]
[GOAL]
case inr.intro.intro.intro.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ ↑a' ∣ ↑4 * ↑(2 ^ e) * ↑a'
[PROOFSTEP]
exact
  dvd_mul_left (a' : ℤ)
    (↑4 * ↑(2 ^ e))
      -- porting note: In mathlib3, it was written `cases' e`. In Lean 4, this resulted in the choice
        -- of a name other than e (for the case distinction of line 482) so we indicate the name
        -- to use explicitly.
[GOAL]
case inr.intro.intro.intro.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ ↑χ₈ ↑b ^ e = ↑χ₈ ↑(b % (4 * a)) ^ e
[PROOFSTEP]
cases' e with e
[GOAL]
case inr.intro.intro.intro.e_a.zero
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
ha₂ : a = 2 ^ zero * a'
⊢ ↑χ₈ ↑b ^ zero = ↑χ₈ ↑(b % (4 * a)) ^ zero
[PROOFSTEP]
rfl
[GOAL]
case inr.intro.intro.intro.e_a.succ
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = 2 ^ succ e * a'
⊢ ↑χ₈ ↑b ^ succ e = ↑χ₈ ↑(b % (4 * a)) ^ succ e
[PROOFSTEP]
rw [χ₈_nat_mod_eight, χ₈_nat_mod_eight (b % (4 * a)), mod_mod_of_dvd b]
[GOAL]
case inr.intro.intro.intro.e_a.succ
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = 2 ^ succ e * a'
⊢ 8 ∣ 4 * a
[PROOFSTEP]
use 2 ^ e * a'
[GOAL]
case h
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = 2 ^ succ e * a'
⊢ 4 * a = 8 * (2 ^ e * a')
[PROOFSTEP]
rw [ha₂, Nat.pow_succ]
[GOAL]
case h
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = 2 ^ succ e * a'
⊢ 4 * (2 ^ e * 2 * a') = 8 * (2 ^ e * a')
[PROOFSTEP]
ring
[GOAL]
a : ℤ
b : ℕ
hb : Odd b
⊢ J(a | b) = J(a | b % (4 * Int.natAbs a))
[PROOFSTEP]
cases' Int.natAbs_eq a with ha ha
[GOAL]
case inl
a : ℤ
b : ℕ
hb : Odd b
ha : a = ↑(Int.natAbs a)
⊢ J(a | b) = J(a | b % (4 * Int.natAbs a))
[PROOFSTEP]
nth_rw 2 [ha]
[GOAL]
case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑(Int.natAbs a)
⊢ J(a | b) = J(a | b % (4 * Int.natAbs a))
[PROOFSTEP]
nth_rw 2 [ha]
[GOAL]
case inl
a : ℤ
b : ℕ
hb : Odd b
ha : a = ↑(Int.natAbs a)
⊢ J(a | b) = J(↑(Int.natAbs a) | b % (4 * Int.natAbs a))
[PROOFSTEP]
nth_rw 1 [ha]
[GOAL]
case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑(Int.natAbs a)
⊢ J(a | b) = J(-↑(Int.natAbs a) | b % (4 * Int.natAbs a))
[PROOFSTEP]
nth_rw 1 [ha]
[GOAL]
case inl
a : ℤ
b : ℕ
hb : Odd b
ha : a = ↑(Int.natAbs a)
⊢ J(↑(Int.natAbs a) | b) = J(↑(Int.natAbs a) | b % (4 * Int.natAbs a))
[PROOFSTEP]
exact mod_right' a.natAbs hb
[GOAL]
case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑(Int.natAbs a)
⊢ J(-↑(Int.natAbs a) | b) = J(-↑(Int.natAbs a) | b % (4 * Int.natAbs a))
[PROOFSTEP]
have hb' : Odd (b % (4 * a.natAbs)) := hb.mod_even (Even.mul_right (by norm_num) _)
[GOAL]
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑(Int.natAbs a)
⊢ Even 4
[PROOFSTEP]
norm_num
[GOAL]
case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑(Int.natAbs a)
hb' : Odd (b % (4 * Int.natAbs a))
⊢ J(-↑(Int.natAbs a) | b) = J(-↑(Int.natAbs a) | b % (4 * Int.natAbs a))
[PROOFSTEP]
rw [jacobiSym.neg _ hb, jacobiSym.neg _ hb', mod_right' _ hb, χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * _)),
  mod_mod_of_dvd b (dvd_mul_right 4 _)]
