[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 _)]


[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ quadraticCharFun F a = 0 ↔ a = 0
[PROOFSTEP]
simp only [quadraticCharFun]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0
[PROOFSTEP]
simp only [ha, eq_self_iff_true, if_true]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0
[PROOFSTEP]
simp only [ha, if_false, iff_false_iff]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ ¬(if IsSquare a then 1 else -1) = 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
h✝ : IsSquare a
⊢ ¬1 = 0
[PROOFSTEP]
simp only [neg_eq_zero, one_ne_zero, not_false_iff]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
h✝ : ¬IsSquare a
⊢ ¬-1 = 0
[PROOFSTEP]
simp only [neg_eq_zero, one_ne_zero, not_false_iff]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ quadraticCharFun F 0 = 0
[PROOFSTEP]
simp only [quadraticCharFun, eq_self_iff_true, if_true, id.def]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ quadraticCharFun F 1 = 1
[PROOFSTEP]
simp only [quadraticCharFun, one_ne_zero, isSquare_one, if_true, if_false, id.def]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F = 2
a : F
ha : a ≠ 0
⊢ quadraticCharFun F a = 1
[PROOFSTEP]
simp only [quadraticCharFun, ha, if_false, ite_eq_left_iff]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F = 2
a : F
ha : a ≠ 0
⊢ ¬IsSquare a → False
[PROOFSTEP]
exact fun h => h (FiniteField.isSquare_of_char_two hF a)
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp only [quadraticCharFun, ha, if_false]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (if IsSquare a then 1 else -1) = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp_rw [FiniteField.isSquare_iff hF ha]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
rw [ha, zero_mul, quadraticCharFun_zero, zero_mul]
  -- now `a ≠ 0`
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
by_cases hb : b = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
rw [hb, mul_zero, quadraticCharFun_zero, mul_zero]
  -- now `a ≠ 0` and `b ≠ 0`
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
have hab := mul_ne_zero ha hb
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
by_cases hF : ringChar F = 2
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
rw [quadraticCharFun_eq_one_of_char_two hF ha, quadraticCharFun_eq_one_of_char_two hF hb,
  quadraticCharFun_eq_one_of_char_two hF hab, mul_one]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
rw [quadraticCharFun_eq_pow_of_char_ne_two hF ha, quadraticCharFun_eq_pow_of_char_ne_two hF hb,
  quadraticCharFun_eq_pow_of_char_ne_two hF hab, mul_pow]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
cases' FiniteField.pow_dichotomy hF hb with hb' hb'
[GOAL]
case neg.inl
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = 1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp only [hb', mul_one, eq_self_iff_true, if_true]
[GOAL]
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
have h := Ring.neg_one_ne_one_of_char_ne_two hF
[GOAL]
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp only [hb', h, mul_neg, mul_one, if_false, ite_mul, neg_mul]
[GOAL]
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
⊢ (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) = -if a ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
cases' FiniteField.pow_dichotomy hF ha with ha' ha'
[GOAL]
case neg.inr.inl
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
ha' : a ^ (Fintype.card F / 2) = 1
⊢ (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) = -if a ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp only [ha', h, neg_neg, eq_self_iff_true, if_true, if_false]
[GOAL]
case neg.inr.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
ha' : a ^ (Fintype.card F / 2) = -1
⊢ (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) = -if a ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp only [ha', h, neg_neg, eq_self_iff_true, if_true, if_false]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬IsUnit a
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := quadraticCharFun F, map_one' := (_ : quadraticCharFun F 1 = 1) },
          map_mul' := (_ : ∀ (a b : F), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b) })
      a =
    0
[PROOFSTEP]
rw [of_not_not (mt Ne.isUnit ha)]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬IsUnit a
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := quadraticCharFun F, map_one' := (_ : quadraticCharFun F 1 = 1) },
          map_mul' := (_ : ∀ (a b : F), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b) })
      0 =
    0
[PROOFSTEP]
exact quadraticCharFun_zero
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ ↑(quadraticChar F) 0 = 0
[PROOFSTEP]
simp only [quadraticChar_apply, quadraticCharFun_zero]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ ↑(quadraticChar F) a = 1 ↔ IsSquare a
[PROOFSTEP]
simp only [quadraticChar_apply, quadraticCharFun, ha, (by decide : (-1 : ℤ) ≠ 1), if_false, ite_eq_left_iff, imp_false,
  Classical.not_not]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ ↑(quadraticChar F) (a ^ 2) = 1
[PROOFSTEP]
simp only [quadraticCharFun, ha, pow_eq_zero_iff, Nat.succ_pos', IsSquare_sq, if_true, if_false, quadraticChar_apply]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ ↑(quadraticChar F) a ^ 2 = 1
[PROOFSTEP]
erw [pow_two, ← map_mul (quadraticChar F) a, ← pow_two]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ ↑(quadraticChar F) (a ^ 2) = 1
[PROOFSTEP]
apply quadraticChar_sq_one' ha
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ ↑(quadraticChar F) a = -1 ↔ ¬↑(quadraticChar F) a = 1
[PROOFSTEP]
refine' ⟨fun h => _, fun h₂ => (or_iff_right h₂).mp (quadraticChar_dichotomy ha)⟩
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
h : ↑(quadraticChar F) a = -1
⊢ ¬↑(quadraticChar F) a = 1
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
h : ↑(quadraticChar F) a = -1
⊢ ¬-1 = 1
[PROOFSTEP]
norm_num
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ ↑(quadraticChar F) a = -1 ↔ ¬IsSquare a
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ ↑(quadraticChar F) a = -1 ↔ ¬IsSquare a
[PROOFSTEP]
simp only [ha, isSquare_zero, MulChar.map_zero, zero_eq_neg, one_ne_zero, not_true]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ ↑(quadraticChar F) a = -1 ↔ ¬IsSquare a
[PROOFSTEP]
rw [quadraticChar_eq_neg_one_iff_not_one ha, quadraticChar_one_iff_isSquare ha]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
⊢ ↑(↑(quadraticChar F) a) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a = 0
⊢ ↑(↑(quadraticChar F) a) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
have : 0 < Fintype.card F / 2 := Nat.div_pos Fintype.one_lt_card two_pos
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a = 0
this : 0 < Fintype.card F / 2
⊢ ↑(↑(quadraticChar F) a) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
simp only [ha, zero_pow this, quadraticChar_apply, quadraticCharFun_zero, Int.cast_zero]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
⊢ ↑(↑(quadraticChar F) a) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
rw [quadraticChar_eq_pow_of_char_ne_two hF ha]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
⊢ ↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
by_cases ha' : a ^ (Fintype.card F / 2) = 1
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
ha' : a ^ (Fintype.card F / 2) = 1
⊢ ↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
simp only [ha', eq_self_iff_true, if_true, Int.cast_one]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
⊢ ↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
have ha'' := Or.resolve_left (FiniteField.pow_dichotomy hF ha) ha'
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
ha'' : a ^ (Fintype.card F / 2) = -1
⊢ ↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
simp only [ha'', Int.cast_ite, Int.cast_one, Int.cast_neg, ite_eq_right_iff]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
ha'' : a ^ (Fintype.card F / 2) = -1
⊢ -1 = 1 → 1 = -1
[PROOFSTEP]
exact Eq.symm
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ IsQuadratic (quadraticChar F)
[PROOFSTEP]
intro a
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ ↑(quadraticChar F) a = 0 ∨ ↑(quadraticChar F) a = 1 ∨ ↑(quadraticChar F) a = -1
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ ↑(quadraticChar F) a = 0 ∨ ↑(quadraticChar F) a = 1 ∨ ↑(quadraticChar F) a = -1
[PROOFSTEP]
left
[GOAL]
case pos.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ ↑(quadraticChar F) a = 0
[PROOFSTEP]
rw [ha]
[GOAL]
case pos.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ ↑(quadraticChar F) 0 = 0
[PROOFSTEP]
exact quadraticChar_zero
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ ↑(quadraticChar F) a = 0 ∨ ↑(quadraticChar F) a = 1 ∨ ↑(quadraticChar F) a = -1
[PROOFSTEP]
right
[GOAL]
case neg.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ ↑(quadraticChar F) a = 1 ∨ ↑(quadraticChar F) a = -1
[PROOFSTEP]
exact quadraticChar_dichotomy ha
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ IsNontrivial (quadraticChar F)
[PROOFSTEP]
rcases quadraticChar_exists_neg_one hF with ⟨a, ha⟩
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
⊢ IsNontrivial (quadraticChar F)
[PROOFSTEP]
have hu : IsUnit a := by by_contra hf; rw [MulChar.map_nonunit _ hf] at ha ; norm_num at ha
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
⊢ IsUnit a
[PROOFSTEP]
by_contra hf
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
hf : ¬IsUnit a
⊢ False
[PROOFSTEP]
rw [MulChar.map_nonunit _ hf] at ha
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : 0 = -1
hf : ¬IsUnit a
⊢ False
[PROOFSTEP]
norm_num at ha
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
hu : IsUnit a
⊢ IsNontrivial (quadraticChar F)
[PROOFSTEP]
refine' ⟨hu.unit, (_ : quadraticChar F a ≠ 1)⟩
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
hu : IsUnit a
⊢ ↑(quadraticChar F) a ≠ 1
[PROOFSTEP]
rw [ha]
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
hu : IsUnit a
⊢ -1 ≠ 1
[PROOFSTEP]
norm_num
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
⊢ ↑(Finset.card (Set.toFinset {x | x ^ 2 = a})) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
by_cases h₀ : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : a = 0
⊢ ↑(Finset.card (Set.toFinset {x | x ^ 2 = a})) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
simp only [h₀, pow_eq_zero_iff, Nat.succ_pos', Int.ofNat_succ, Int.ofNat_zero, MulChar.map_zero,
  Set.setOf_eq_eq_singleton, Set.toFinset_card, Set.card_singleton]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
⊢ ↑(Finset.card (Set.toFinset {x | x ^ 2 = a})) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
set s := {x : F | x ^ 2 = a}.toFinset
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
⊢ ↑(Finset.card s) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
by_cases h : IsSquare a
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : IsSquare a
⊢ ↑(Finset.card s) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
rw [(quadraticChar_one_iff_isSquare h₀).mpr h]
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : IsSquare a
⊢ ↑(Finset.card s) = 1 + 1
[PROOFSTEP]
rcases h with ⟨b, h⟩
[GOAL]
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h : a = b * b
⊢ ↑(Finset.card s) = 1 + 1
[PROOFSTEP]
rw [h, mul_self_eq_zero] at h₀
[GOAL]
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
⊢ ↑(Finset.card s) = 1 + 1
[PROOFSTEP]
have h₁ : s = [b, -b].toFinset := by
  ext x
  simp only [Finset.mem_filter, Finset.mem_univ, true_and_iff, List.toFinset_cons, List.toFinset_nil, insert_emptyc_eq,
    Finset.mem_insert, Finset.mem_singleton]
  rw [← pow_two] at h
  simp only [h, Set.toFinset_setOf, Finset.mem_univ, Finset.mem_filter, true_and]
  constructor
  · exact eq_or_eq_neg_of_sq_eq_sq _ _
  · rintro (h₂ | h₂) <;> rw [h₂]
    simp only [neg_sq]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
⊢ s = List.toFinset [b, -b]
[PROOFSTEP]
ext x
[GOAL]
case a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
x : F
⊢ x ∈ s ↔ x ∈ List.toFinset [b, -b]
[PROOFSTEP]
simp only [Finset.mem_filter, Finset.mem_univ, true_and_iff, List.toFinset_cons, List.toFinset_nil, insert_emptyc_eq,
  Finset.mem_insert, Finset.mem_singleton]
[GOAL]
case a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
x : F
⊢ x ∈ Set.toFinset {x | x ^ 2 = a} ↔ x = b ∨ x = -b
[PROOFSTEP]
rw [← pow_two] at h
[GOAL]
case a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
⊢ x ∈ Set.toFinset {x | x ^ 2 = a} ↔ x = b ∨ x = -b
[PROOFSTEP]
simp only [h, Set.toFinset_setOf, Finset.mem_univ, Finset.mem_filter, true_and]
[GOAL]
case a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
⊢ x ^ 2 = b ^ 2 ↔ x = b ∨ x = -b
[PROOFSTEP]
constructor
[GOAL]
case a.mp
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
⊢ x ^ 2 = b ^ 2 → x = b ∨ x = -b
[PROOFSTEP]
exact eq_or_eq_neg_of_sq_eq_sq _ _
[GOAL]
case a.mpr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
⊢ x = b ∨ x = -b → x ^ 2 = b ^ 2
[PROOFSTEP]
rintro (h₂ | h₂)
[GOAL]
case a.mpr.inl
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
h₂ : x = b
⊢ x ^ 2 = b ^ 2
[PROOFSTEP]
rw [h₂]
[GOAL]
case a.mpr.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
h₂ : x = -b
⊢ x ^ 2 = b ^ 2
[PROOFSTEP]
rw [h₂]
[GOAL]
case a.mpr.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
h₂ : x = -b
⊢ (-b) ^ 2 = b ^ 2
[PROOFSTEP]
simp only [neg_sq]
[GOAL]
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
h₁ : s = List.toFinset [b, -b]
⊢ ↑(Finset.card s) = 1 + 1
[PROOFSTEP]
norm_cast
[GOAL]
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
h₁ : s = List.toFinset [b, -b]
⊢ Finset.card s = 1 + 1
[PROOFSTEP]
rw [h₁, List.toFinset_cons, List.toFinset_cons, List.toFinset_nil]
[GOAL]
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
h₁ : s = List.toFinset [b, -b]
⊢ Finset.card (insert b (insert (-b) ∅)) = 1 + 1
[PROOFSTEP]
exact Finset.card_doubleton (Ne.symm (mt (Ring.eq_self_iff_eq_zero_of_char_ne_two hF).mp h₀))
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬IsSquare a
⊢ ↑(Finset.card s) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
rw [quadraticChar_neg_one_iff_not_isSquare.mpr h]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬IsSquare a
⊢ ↑(Finset.card s) = -1 + 1
[PROOFSTEP]
simp only [Int.coe_nat_eq_zero, Finset.card_eq_zero, Set.toFinset_card, Fintype.card_ofFinset, Set.mem_setOf_eq,
  add_left_neg]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬IsSquare a
⊢ Set.toFinset {x | x ^ 2 = a} = ∅
[PROOFSTEP]
ext x
[GOAL]
case neg.a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬IsSquare a
x : F
⊢ x ∈ Set.toFinset {x | x ^ 2 = a} ↔ x ∈ ∅
[PROOFSTEP]
simp only [iff_false_iff, Finset.mem_filter, Finset.mem_univ, true_and_iff, Finset.not_mem_empty, (Set.mem_toFinset),
  Set.mem_setOf]
[GOAL]
case neg.a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬IsSquare a
x : F
⊢ ¬x ^ 2 = a
[PROOFSTEP]
rw [isSquare_iff_exists_sq] at h
[GOAL]
case neg.a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬∃ c, a = c ^ 2
x : F
⊢ ¬x ^ 2 = a
[PROOFSTEP]
exact fun h' => h ⟨_, h'.symm⟩
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ ↑(quadraticChar F) (-1) = ↑χ₄ ↑(Fintype.card F)
[PROOFSTEP]
have h := quadraticChar_eq_pow_of_char_ne_two hF (neg_ne_zero.mpr one_ne_zero)
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
h : ↑(quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1
⊢ ↑(quadraticChar F) (-1) = ↑χ₄ ↑(Fintype.card F)
[PROOFSTEP]
rw [h, χ₄_eq_neg_one_pow (FiniteField.odd_card_of_char_ne_two hF)]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
h : ↑(quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1
⊢ (if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1) = (-1) ^ (Fintype.card F / 2)
[PROOFSTEP]
set n := Fintype.card F / 2
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
n : ℕ := Fintype.card F / 2
h : ↑(quadraticChar F) (-1) = if (-1) ^ n = 1 then 1 else -1
⊢ (if (-1) ^ n = 1 then 1 else -1) = (-1) ^ n
[PROOFSTEP]
cases' Nat.even_or_odd n with h₂ h₂
[GOAL]
case inl
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
n : ℕ := Fintype.card F / 2
h : ↑(quadraticChar F) (-1) = if (-1) ^ n = 1 then 1 else -1
h₂ : Even n
⊢ (if (-1) ^ n = 1 then 1 else -1) = (-1) ^ n
[PROOFSTEP]
simp only [Even.neg_one_pow h₂, eq_self_iff_true, if_true]
[GOAL]
case inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
n : ℕ := Fintype.card F / 2
h : ↑(quadraticChar F) (-1) = if (-1) ^ n = 1 then 1 else -1
h₂ : Odd n
⊢ (if (-1) ^ n = 1 then 1 else -1) = (-1) ^ n
[PROOFSTEP]
simp only [Odd.neg_one_pow h₂, Ring.neg_one_ne_one_of_char_ne_two hF, ite_false]
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
classical
  -- suggested by the linter (instead of `[DecidableEq F]`)
by_cases hF : ringChar F = 2
· simp only [FiniteField.isSquare_of_char_two hF, Ne.def, true_iff_iff]
  exact fun hf => one_ne_zero <| (Nat.odd_of_mod_four_eq_three hf).symm.trans <| FiniteField.even_card_of_char_two hF
· have h₁ := FiniteField.odd_card_of_char_ne_two hF
  rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (one_ne_zero' F)), quadraticChar_neg_one hF,
    χ₄_nat_eq_if_mod_four, h₁]
  simp only [Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false,
    Classical.not_not]
  exact ⟨fun h => ne_of_eq_of_ne h (by decide : 1 ≠ 3), Or.resolve_right (Nat.odd_mod_four_iff.mp h₁)⟩
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
by_cases hF : ringChar F = 2
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
simp only [FiniteField.isSquare_of_char_two hF, Ne.def, true_iff_iff]
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ ¬Fintype.card F % 4 = 3
[PROOFSTEP]
exact fun hf => one_ne_zero <| (Nat.odd_of_mod_four_eq_three hf).symm.trans <| FiniteField.even_card_of_char_two hF
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
have h₁ := FiniteField.odd_card_of_char_ne_two hF
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (one_ne_zero' F)), quadraticChar_neg_one hF,
  χ₄_nat_eq_if_mod_four, h₁]
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ (if 1 = 0 then 0 else if Fintype.card F % 4 = 1 then 1 else -1) = 1 ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
simp only [Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false, Classical.not_not]
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ Fintype.card F % 4 = 1 ↔ ¬Fintype.card F % 4 = 3
[PROOFSTEP]
exact ⟨fun h => ne_of_eq_of_ne h (by decide : 1 ≠ 3), Or.resolve_right (Nat.odd_mod_four_iff.mp h₁)⟩
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
h : Fintype.card F % 4 = 1
⊢ 1 ≠ 3
[PROOFSTEP]
decide