[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
⊢ Multiset.map (fun x => Int.natAbs (valMinAbs (a * ↑x))) (Ico 1 (succ (p / 2))).val =
    Multiset.map (fun a => a) (Ico 1 (succ (p / 2))).val
[PROOFSTEP]
have he : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2 := by
  simp (config := { contextual := true }) [Nat.lt_succ_iff, Nat.succ_le_iff, pos_iff_ne_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
⊢ ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
[PROOFSTEP]
simp (config := { contextual := true }) [Nat.lt_succ_iff, Nat.succ_le_iff, pos_iff_ne_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
⊢ Multiset.map (fun x => Int.natAbs (valMinAbs (a * ↑x))) (Ico 1 (succ (p / 2))).val =
    Multiset.map (fun a => a) (Ico 1 (succ (p / 2))).val
[PROOFSTEP]
have hep : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x < p := fun hx =>
  lt_of_le_of_lt (he hx).2 (Nat.div_lt_self hp.1.pos (by decide))
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
x✝ : ℕ
hx : x✝ ∈ Ico 1 (succ (p / 2))
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
⊢ Multiset.map (fun x => Int.natAbs (valMinAbs (a * ↑x))) (Ico 1 (succ (p / 2))).val =
    Multiset.map (fun a => a) (Ico 1 (succ (p / 2))).val
[PROOFSTEP]
have hpe : ∀ {x}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x := fun hx hpx =>
  not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero (he hx).1) hpx) (hep hx)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
⊢ Multiset.map (fun x => Int.natAbs (valMinAbs (a * ↑x))) (Ico 1 (succ (p / 2))).val =
    Multiset.map (fun a => a) (Ico 1 (succ (p / 2))).val
[PROOFSTEP]
have hmem : ∀ (x : ℕ) (hx : x ∈ Ico 1 (p / 2).succ), (a * x : ZMod p).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ :=
  by
  intro x hx
  simp [hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hx, lt_succ_iff, succ_le_iff, pos_iff_ne_zero,
    natAbs_valMinAbs_le _]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
⊢ ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
[PROOFSTEP]
intro x hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
x : ℕ
hx : x ∈ Ico 1 (succ (p / 2))
⊢ Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
[PROOFSTEP]
simp [hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hx, lt_succ_iff, succ_le_iff, pos_iff_ne_zero, natAbs_valMinAbs_le _]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
⊢ Multiset.map (fun x => Int.natAbs (valMinAbs (a * ↑x))) (Ico 1 (succ (p / 2))).val =
    Multiset.map (fun a => a) (Ico 1 (succ (p / 2))).val
[PROOFSTEP]
have hsurj : ∀ (b : ℕ) (hb : b ∈ Ico 1 (p / 2).succ), ∃ x ∈ Ico 1 (p / 2).succ, b = (a * x : ZMod p).valMinAbs.natAbs :=
  by
  intro b hb
  refine' ⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨_, _⟩, _⟩
  · apply Nat.pos_of_ne_zero
    simp only [div_eq_mul_inv, hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hb, not_false_iff, valMinAbs_eq_zero,
      inv_eq_zero, Int.natAbs_eq_zero, Ne.def, _root_.mul_eq_zero, or_self_iff]
  · apply lt_succ_of_le; apply natAbs_valMinAbs_le
  · rw [nat_cast_natAbs_valMinAbs]
    split_ifs
    ·
      erw [mul_div_cancel' _ hap, valMinAbs_def_pos, val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2),
        Int.natAbs_ofNat]
    ·
      erw [mul_neg, mul_div_cancel' _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos, val_cast_of_lt (hep hb),
        if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_ofNat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
⊢ ∀ (b : ℕ), b ∈ Ico 1 (succ (p / 2)) → ∃ x, x ∈ Ico 1 (succ (p / 2)) ∧ b = Int.natAbs (valMinAbs (a * ↑x))
[PROOFSTEP]
intro b hb
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
b : ℕ
hb : b ∈ Ico 1 (succ (p / 2))
⊢ ∃ x, x ∈ Ico 1 (succ (p / 2)) ∧ b = Int.natAbs (valMinAbs (a * ↑x))
[PROOFSTEP]
refine' ⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨_, _⟩, _⟩
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
b : ℕ
hb : b ∈ Ico 1 (succ (p / 2))
⊢ 1 ≤ Int.natAbs (valMinAbs (↑b / a))
[PROOFSTEP]
apply Nat.pos_of_ne_zero
[GOAL]
case refine'_1.a
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
b : ℕ
hb : b ∈ Ico 1 (succ (p / 2))
⊢ Int.natAbs (valMinAbs (↑b / a)) ≠ 0
[PROOFSTEP]
simp only [div_eq_mul_inv, hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hb, not_false_iff, valMinAbs_eq_zero,
  inv_eq_zero, Int.natAbs_eq_zero, Ne.def, _root_.mul_eq_zero, or_self_iff]
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
b : ℕ
hb : b ∈ Ico 1 (succ (p / 2))
⊢ Int.natAbs (valMinAbs (↑b / a)) < succ (p / 2)
[PROOFSTEP]
apply lt_succ_of_le
[GOAL]
case refine'_2.a
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
b : ℕ
hb : b ∈ Ico 1 (succ (p / 2))
⊢ Int.natAbs (valMinAbs (↑b / a)) ≤ p / 2
[PROOFSTEP]
apply natAbs_valMinAbs_le
[GOAL]
case refine'_3
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
b : ℕ
hb : b ∈ Ico 1 (succ (p / 2))
⊢ b = Int.natAbs (valMinAbs (a * ↑(Int.natAbs (valMinAbs (↑b / a)))))
[PROOFSTEP]
rw [nat_cast_natAbs_valMinAbs]
[GOAL]
case refine'_3
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
b : ℕ
hb : b ∈ Ico 1 (succ (p / 2))
⊢ b = Int.natAbs (valMinAbs (a * if val (↑b / a) ≤ p / 2 then ↑b / a else -(↑b / a)))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
b : ℕ
hb : b ∈ Ico 1 (succ (p / 2))
h✝ : val (↑b / a) ≤ p / 2
⊢ b = Int.natAbs (valMinAbs (a * (↑b / a)))
[PROOFSTEP]
erw [mul_div_cancel' _ hap, valMinAbs_def_pos, val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2),
  Int.natAbs_ofNat]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
b : ℕ
hb : b ∈ Ico 1 (succ (p / 2))
h✝ : ¬val (↑b / a) ≤ p / 2
⊢ b = Int.natAbs (valMinAbs (a * -(↑b / a)))
[PROOFSTEP]
erw [mul_neg, mul_div_cancel' _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos, val_cast_of_lt (hep hb),
  if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_ofNat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
hsurj : ∀ (b : ℕ), b ∈ Ico 1 (succ (p / 2)) → ∃ x, x ∈ Ico 1 (succ (p / 2)) ∧ b = Int.natAbs (valMinAbs (a * ↑x))
⊢ Multiset.map (fun x => Int.natAbs (valMinAbs (a * ↑x))) (Ico 1 (succ (p / 2))).val =
    Multiset.map (fun a => a) (Ico 1 (succ (p / 2))).val
[PROOFSTEP]
simp only [← exists_prop] at hsurj 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (succ (p / 2)) → ¬p ∣ x
hmem : ∀ (x : ℕ), x ∈ Ico 1 (succ (p / 2)) → Int.natAbs (valMinAbs (a * ↑x)) ∈ Ico 1 (succ (p / 2))
hsurj : ∀ (b : ℕ), b ∈ Ico 1 (succ (p / 2)) → ∃ x _h, b = Int.natAbs (valMinAbs (a * ↑x))
⊢ Multiset.map (fun x => Int.natAbs (valMinAbs (a * ↑x))) (Ico 1 (succ (p / 2))).val =
    Multiset.map (fun a => a) (Ico 1 (succ (p / 2))).val
[PROOFSTEP]
exact
  Multiset.map_eq_map_of_bij_of_nodup _ _ (Finset.nodup _) (Finset.nodup _)
    (fun x _ => (a * x : ZMod p).valMinAbs.natAbs) hmem (fun _ _ => rfl)
    (inj_on_of_surj_on_of_card_le _ hmem hsurj le_rfl) hsurj
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑(a ^ (p / 2)) * ↑(p / 2)! = ↑(∏ x in Ico 1 (succ (p / 2)), a * ↑x)
[PROOFSTEP]
rw [prod_mul_distrib, ← prod_natCast, prod_Ico_id_eq_factorial, prod_const, card_Ico, succ_sub_one]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑(a ^ (p / 2)) * ↑(p / 2)! = ↑(a ^ (p / 2) * ↑(p / 2)!)
[PROOFSTEP]
simp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑(∏ x in Ico 1 (succ (p / 2)), a * ↑x) = ∏ x in Ico 1 (succ (p / 2)), ↑(val (↑a * ↑x))
[PROOFSTEP]
simp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (succ (p / 2))
⊢ ↑(val (↑a * ↑x✝¹)) = (if val (↑a * ↑x✝¹) ≤ p / 2 then 1 else -1) * ↑(Int.natAbs (valMinAbs (↑a * ↑x✝¹)))
[PROOFSTEP]
simp only [nat_cast_natAbs_valMinAbs]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (succ (p / 2))
⊢ ↑(val (↑a * ↑x✝¹)) =
    (if val (↑a * ↑x✝¹) ≤ p / 2 then 1 else -1) * if val (↑a * ↑x✝¹) ≤ p / 2 then ↑a * ↑x✝¹ else -(↑a * ↑x✝¹)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (succ (p / 2))
h✝ : val (↑a * ↑x✝¹) ≤ p / 2
⊢ ↑(val (↑a * ↑x✝¹)) = 1 * (↑a * ↑x✝¹)
[PROOFSTEP]
simp
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (succ (p / 2))
h✝ : ¬val (↑a * ↑x✝¹) ≤ p / 2
⊢ ↑(val (↑a * ↑x✝¹)) = -1 * -(↑a * ↑x✝¹)
[PROOFSTEP]
simp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ∏ x in Ico 1 (succ (p / 2)), (if val (↑a * ↑x) ≤ p / 2 then 1 else -1) * ↑(Int.natAbs (valMinAbs (↑a * ↑x))) =
    (-1) ^ Finset.card (filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2)))) *
      ∏ x in Ico 1 (succ (p / 2)), ↑(Int.natAbs (valMinAbs (↑a * ↑x)))
[PROOFSTEP]
have :
  (∏ x in Ico 1 (p / 2).succ, if (a * x : ZMod p).val ≤ p / 2 then (1 : ZMod p) else -1) =
    ∏ x in (Ico 1 (p / 2).succ).filter fun x : ℕ => ¬(a * x : ZMod p).val ≤ p / 2, -1 :=
  prod_bij_ne_one (fun x _ _ => x) (fun x => by split_ifs <;> simp_all (config := { contextual := true }))
    (fun _ _ _ _ _ _ => id) (fun b h _ => ⟨b, by simp_all [-not_le]⟩) (by intros; split_ifs at * <;> simp_all)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x : ℕ
⊢ ∀ (h₁ : x ∈ Ico 1 (succ (p / 2))) (h₂ : (if val (↑a * ↑x) ≤ p / 2 then 1 else -1) ≠ 1),
    (fun x x_1 x_2 => x) x h₁ h₂ ∈ filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2)))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x : ℕ
h✝ : val (↑a * ↑x) ≤ p / 2
⊢ ∀ (h₁ : x ∈ Ico 1 (succ (p / 2))) (h₂ : (if val (↑a * ↑x) ≤ p / 2 then 1 else -1) ≠ 1),
    (fun x x_1 x_2 => x) x h₁ h₂ ∈ filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2)))
[PROOFSTEP]
simp_all (config := { contextual := true })
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x : ℕ
h✝ : ¬val (↑a * ↑x) ≤ p / 2
⊢ ∀ (h₁ : x ∈ Ico 1 (succ (p / 2))) (h₂ : (if val (↑a * ↑x) ≤ p / 2 then 1 else -1) ≠ 1),
    (fun x x_1 x_2 => x) x h₁ h₂ ∈ filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2)))
[PROOFSTEP]
simp_all (config := { contextual := true })
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
b : ℕ
h : b ∈ filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2)))
x✝ : -1 ≠ 1
⊢ ∃ h₁ h₂, b = (fun x x_1 x_2 => x) b h₁ h₂
[PROOFSTEP]
simp_all [-not_le]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ∀ (a_1 : ℕ),
    a_1 ∈ Ico 1 (succ (p / 2)) →
      (if val (↑a * ↑a_1) ≤ p / 2 then 1 else -1) ≠ 1 → (if val (↑a * ↑a_1) ≤ p / 2 then 1 else -1) = -1
[PROOFSTEP]
intros
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
a✝ : ℕ
h₁✝ : a✝ ∈ Ico 1 (succ (p / 2))
h₂✝ : (if val (↑a * ↑a✝) ≤ p / 2 then 1 else -1) ≠ 1
⊢ (if val (↑a * ↑a✝) ≤ p / 2 then 1 else -1) = -1
[PROOFSTEP]
split_ifs at *
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
a✝ : ℕ
h₁✝ : a✝ ∈ Ico 1 (succ (p / 2))
h✝ : val (↑a * ↑a✝) ≤ p / 2
h₂✝ : 1 ≠ 1
⊢ 1 = -1
[PROOFSTEP]
simp_all
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
a✝ : ℕ
h₁✝ : a✝ ∈ Ico 1 (succ (p / 2))
h✝ : ¬val (↑a * ↑a✝) ≤ p / 2
h₂✝ : -1 ≠ 1
⊢ -1 = -1
[PROOFSTEP]
simp_all
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
this :
  (∏ x in Ico 1 (succ (p / 2)), if val (↑a * ↑x) ≤ p / 2 then 1 else -1) =
    ∏ x in filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2))), -1
⊢ ∏ x in Ico 1 (succ (p / 2)), (if val (↑a * ↑x) ≤ p / 2 then 1 else -1) * ↑(Int.natAbs (valMinAbs (↑a * ↑x))) =
    (-1) ^ Finset.card (filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2)))) *
      ∏ x in Ico 1 (succ (p / 2)), ↑(Int.natAbs (valMinAbs (↑a * ↑x)))
[PROOFSTEP]
rw [prod_mul_distrib, this]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
this :
  (∏ x in Ico 1 (succ (p / 2)), if val (↑a * ↑x) ≤ p / 2 then 1 else -1) =
    ∏ x in filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2))), -1
⊢ (∏ x in filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2))), -1) *
      ∏ x in Ico 1 (succ (p / 2)), ↑(Int.natAbs (valMinAbs (↑a * ↑x))) =
    (-1) ^ Finset.card (filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2)))) *
      ∏ x in Ico 1 (succ (p / 2)), ↑(Int.natAbs (valMinAbs (↑a * ↑x)))
[PROOFSTEP]
simp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ (-1) ^ Finset.card (filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2)))) *
      ∏ x in Ico 1 (succ (p / 2)), ↑(Int.natAbs (valMinAbs (↑a * ↑x))) =
    (-1) ^ Finset.card (filter (fun x => ¬val (↑a * ↑x) ≤ p / 2) (Ico 1 (succ (p / 2)))) * ↑(p / 2)!
[PROOFSTEP]
rw [← prod_natCast, Finset.prod_eq_multiset_prod, Ico_map_valMinAbs_natAbs_eq_Ico_map_id p a hap, ←
  Finset.prod_eq_multiset_prod, prod_Ico_id_eq_factorial]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑(p / 2)! ≠ 0
[PROOFSTEP]
rw [Ne.def, CharP.cast_eq_zero_iff (ZMod p) p, hp.1.dvd_factorial, not_le]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ p / 2 < p
[PROOFSTEP]
exact Nat.div_lt_self hp.1.pos (by decide)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! =
    ↑((-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))) * ↑(p / 2)!
[PROOFSTEP]
simpa using gauss_lemma_aux₁ p hap
[GOAL]
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
hp : p ≠ 2
ha0 : ↑a ≠ 0
⊢ legendreSym p a = (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))
[PROOFSTEP]
replace hp : Odd p := h.out.odd_of_ne_two hp
[GOAL]
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
⊢ legendreSym p a = (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))
[PROOFSTEP]
have :
  (legendreSym p a : ZMod p) =
    (((-1) ^ ((Ico 1 (p / 2).succ).filter fun x : ℕ => p / 2 < (a * x : ZMod p).val).card : ℤ) : ZMod p) :=
  by rw [legendreSym.eq_pow, gauss_lemma_aux p ha0]
[GOAL]
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
⊢ ↑(legendreSym p a) = ↑((-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))))
[PROOFSTEP]
rw [legendreSym.eq_pow, gauss_lemma_aux p ha0]
[GOAL]
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))))
⊢ legendreSym p a = (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))
[PROOFSTEP]
cases legendreSym.eq_one_or_neg_one p ha0
[GOAL]
case inl
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))))
h✝ : legendreSym p a = 1
⊢ legendreSym p a = (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))
[PROOFSTEP]
cases neg_one_pow_eq_or ℤ ((Ico 1 (p / 2).succ).filter fun x : ℕ => p / 2 < (a * x : ZMod p).val).card
[GOAL]
case inr
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))))
h✝ : legendreSym p a = -1
⊢ legendreSym p a = (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))
[PROOFSTEP]
cases neg_one_pow_eq_or ℤ ((Ico 1 (p / 2).succ).filter fun x : ℕ => p / 2 < (a * x : ZMod p).val).card
[GOAL]
case inl.inl
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))))
h✝¹ : legendreSym p a = 1
h✝ : (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))) = 1
⊢ legendreSym p a = (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))
[PROOFSTEP]
simp_all [ne_neg_self hp one_ne_zero, (ne_neg_self hp one_ne_zero).symm]
[GOAL]
case inl.inr
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))))
h✝¹ : legendreSym p a = 1
h✝ : (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))) = -1
⊢ legendreSym p a = (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))
[PROOFSTEP]
simp_all [ne_neg_self hp one_ne_zero, (ne_neg_self hp one_ne_zero).symm]
[GOAL]
case inr.inl
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))))
h✝¹ : legendreSym p a = -1
h✝ : (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))) = 1
⊢ legendreSym p a = (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))
[PROOFSTEP]
simp_all [ne_neg_self hp one_ne_zero, (ne_neg_self hp one_ne_zero).symm]
[GOAL]
case inr.inr
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))))
h✝¹ : legendreSym p a = -1
h✝ : (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2)))) = -1
⊢ legendreSym p a = (-1) ^ Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))
[PROOFSTEP]
simp_all [ne_neg_self hp one_ne_zero, (ne_neg_self hp one_ne_zero).symm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x in Ico 1 (succ (p / 2)), a * x) = ↑(∑ x in Ico 1 (succ (p / 2)), (a * x % p + p * (a * x / p)))
[PROOFSTEP]
simp only [mod_add_div]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x in Ico 1 (succ (p / 2)), (a * x % p + p * (a * x / p))) =
    ↑(∑ x in Ico 1 (succ (p / 2)), val ↑(a * x)) + ↑(∑ x in Ico 1 (succ (p / 2)), a * x / p)
[PROOFSTEP]
simp only [val_nat_cast]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x in Ico 1 (succ (p / 2)), (a * x % p + p * (a * x / p))) =
    ↑(∑ x in Ico 1 (succ (p / 2)), a * x % p) + ↑(∑ x in Ico 1 (succ (p / 2)), a * x / p)
[PROOFSTEP]
simp [sum_add_distrib, mul_sum.symm, Nat.cast_add, Nat.cast_mul, Nat.cast_sum, hp2]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x in Ico 1 (succ (p / 2)), val ↑(a * x)) =
    ∑ x in Ico 1 (succ (p / 2)), ↑(valMinAbs (↑a * ↑x) + ↑(if val (↑a * ↑x) ≤ p / 2 then 0 else p))
[PROOFSTEP]
simp only [(val_eq_ite_valMinAbs _).symm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x in Ico 1 (succ (p / 2)), val ↑(a * x)) = ∑ x in Ico 1 (succ (p / 2)), ↑↑(val (↑a * ↑x))
[PROOFSTEP]
simp [Nat.cast_sum]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ∑ x in Ico 1 (succ (p / 2)), ↑(valMinAbs (↑a * ↑x) + ↑(if val (↑a * ↑x) ≤ p / 2 then 0 else p)) =
    ↑(Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))) +
      ↑(∑ x in Ico 1 (succ (p / 2)), Int.natAbs (valMinAbs (↑a * ↑x)))
[PROOFSTEP]
simp [add_comm, sum_add_distrib, Finset.sum_ite, hp2, Nat.cast_sum]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))) +
      ↑(∑ x in Ico 1 (succ (p / 2)), Int.natAbs (valMinAbs (↑a * ↑x))) =
    ↑(Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))) + ↑(∑ x in Ico 1 (succ (p / 2)), x)
[PROOFSTEP]
rw [Finset.sum_eq_multiset_sum, Ico_map_valMinAbs_natAbs_eq_Ico_map_id p a hap, ← Finset.sum_eq_multiset_sum]
[GOAL]
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (p % 2 = 1)
a : ℕ
ha2✝ : a % 2 = 1
hap : ↑a ≠ 0
ha2 : ↑a = ↑1
⊢ ↑(Finset.card (filter (fun x => p / 2 < val (↑a * ↑x)) (Ico 1 (succ (p / 2))))) -
      ↑(∑ x in Ico 1 (succ (p / 2)), x * a / p) =
    0
[PROOFSTEP]
simpa [add_left_comm, sub_eq_add_neg, Finset.mul_sum.symm, mul_comm, ha2, Nat.cast_sum, add_neg_eq_iff_eq_add.symm,
  neg_eq_self_mod_two, add_assoc] using Eq.symm (eisenstein_lemma_aux₁ p hap)
[GOAL]
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
⊢ a / b = Finset.card (Ico 1 (succ (a / b)))
[PROOFSTEP]
simp
[GOAL]
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
⊢ x ∈ Ico 1 (succ (a / b)) ↔ x ∈ filter (fun x => x * b ≤ a) (Ico 1 (succ c))
[PROOFSTEP]
have : x * b ≤ a → x ≤ c := fun h => le_trans (by rwa [le_div_iff_mul_le hb0]) hc
[GOAL]
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
h : x * b ≤ a
⊢ x ≤ a / b
[PROOFSTEP]
rwa [le_div_iff_mul_le hb0]
[GOAL]
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
this : x * b ≤ a → x ≤ c
⊢ x ∈ Ico 1 (succ (a / b)) ↔ x ∈ filter (fun x => x * b ≤ a) (Ico 1 (succ c))
[PROOFSTEP]
simp [lt_succ_iff, le_div_iff_mul_le hb0]
[GOAL]
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
this : x * b ≤ a → x ≤ c
⊢ x * b ≤ a → 1 ≤ x → x ≤ c
[PROOFSTEP]
tauto
[GOAL]
p q : ℕ
hp0 : p = 0
⊢ ∑ a in Ico 1 (succ (p / 2)), a * q / p =
    Finset.card (filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
[PROOFSTEP]
simp [hp0, Finset.ext_iff]
[GOAL]
p q : ℕ
hp0 : ¬p = 0
⊢ ∑ a in Ico 1 (succ (p / 2)), Finset.card (filter (fun x => x * p ≤ a * q) (Ico 1 (succ (q / 2)))) =
    Finset.card (filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
[PROOFSTEP]
rw [← card_sigma]
[GOAL]
p q : ℕ
hp0 : ¬p = 0
⊢ Finset.card (Finset.sigma (Ico 1 (succ (p / 2))) fun a => filter (fun x => x * p ≤ a * q) (Ico 1 (succ (q / 2)))) =
    Finset.card (filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
[PROOFSTEP]
exact
  card_congr (fun a _ => ⟨a.1, a.2⟩)
    (by
      simp (config := { contextual := true }) only [mem_filter, mem_sigma, and_self_iff, forall_true_iff, mem_product])
    (fun ⟨_, _⟩ ⟨_, _⟩ => by
      simp (config := { contextual := true }) only [Prod.mk.inj_iff, eq_self_iff_true, and_self_iff, heq_iff_eq,
        forall_true_iff])
    fun ⟨b₁, b₂⟩ h =>
    ⟨⟨b₁, b₂⟩, by
      revert h
      simp (config := { contextual := true }) only [mem_filter, eq_self_iff_true, exists_prop_of_true, mem_sigma,
        and_self_iff, forall_true_iff, mem_product]⟩
[GOAL]
p q : ℕ
hp0 : ¬p = 0
⊢ ∀ (a : (_ : ℕ) × ℕ)
    (ha : a ∈ Finset.sigma (Ico 1 (succ (p / 2))) fun a => filter (fun x => x * p ≤ a * q) (Ico 1 (succ (q / 2)))),
    (fun a x => (a.fst, a.snd)) a ha ∈
      filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2)))
[PROOFSTEP]
simp (config := { contextual := true }) only [mem_filter, mem_sigma, and_self_iff, forall_true_iff, mem_product]
[GOAL]
p q : ℕ
hp0 : ¬p = 0
x✝¹ x✝ : (_ : ℕ) × ℕ
fst✝¹ snd✝¹ fst✝ snd✝ : ℕ
⊢ ∀
    (ha :
      { fst := fst✝¹, snd := snd✝¹ } ∈
        Finset.sigma (Ico 1 (succ (p / 2))) fun a => filter (fun x => x * p ≤ a * q) (Ico 1 (succ (q / 2))))
    (hb :
      { fst := fst✝, snd := snd✝ } ∈
        Finset.sigma (Ico 1 (succ (p / 2))) fun a => filter (fun x => x * p ≤ a * q) (Ico 1 (succ (q / 2)))),
    (fun a x => (a.fst, a.snd)) { fst := fst✝¹, snd := snd✝¹ } ha =
        (fun a x => (a.fst, a.snd)) { fst := fst✝, snd := snd✝ } hb →
      { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
simp (config := { contextual := true }) only [Prod.mk.inj_iff, eq_self_iff_true, and_self_iff, heq_iff_eq,
  forall_true_iff]
[GOAL]
p q : ℕ
hp0 : ¬p = 0
x✝ : ℕ × ℕ
b₁ b₂ : ℕ
h : (b₁, b₂) ∈ filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2)))
⊢ ∃ ha, (fun a x => (a.fst, a.snd)) { fst := b₁, snd := b₂ } ha = (b₁, b₂)
[PROOFSTEP]
revert h
[GOAL]
p q : ℕ
hp0 : ¬p = 0
x✝ : ℕ × ℕ
b₁ b₂ : ℕ
⊢ (b₁, b₂) ∈ filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))) →
    ∃ ha, (fun a x => (a.fst, a.snd)) { fst := b₁, snd := b₂ } ha = (b₁, b₂)
[PROOFSTEP]
simp (config := { contextual := true }) only [mem_filter, eq_self_iff_true, exists_prop_of_true, mem_sigma,
  and_self_iff, forall_true_iff, mem_product]
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
⊢ ∑ a in Ico 1 (succ (p / 2)), a * q / p + ∑ a in Ico 1 (succ (q / 2)), a * p / q = p / 2 * (q / 2)
[PROOFSTEP]
have hswap :
  ((Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ).filter fun x : ℕ × ℕ => x.2 * q ≤ x.1 * p).card =
    ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter fun x : ℕ × ℕ => x.1 * q ≤ x.2 * p).card :=
  card_congr (fun x _ => Prod.swap x)
    (fun ⟨_, _⟩ => by
      simp (config := { contextual := true }) only [mem_filter, and_self_iff, Prod.swap_prod_mk, forall_true_iff,
        mem_product])
    (fun ⟨_, _⟩ ⟨_, _⟩ => by
      simp (config := { contextual := true }) only [Prod.mk.inj_iff, eq_self_iff_true, and_self_iff, Prod.swap_prod_mk,
        forall_true_iff])
    fun ⟨x₁, x₂⟩ h =>
    ⟨⟨x₂, x₁⟩, by
      revert h
      simp (config := { contextual := true }) only [mem_filter, eq_self_iff_true, and_self_iff, exists_prop_of_true,
        Prod.swap_prod_mk, forall_true_iff, mem_product]⟩
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
x✝ : ℕ × ℕ
fst✝ snd✝ : ℕ
⊢ ∀ (ha : (fst✝, snd✝) ∈ filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))),
    (fun x x_1 => Prod.swap x) (fst✝, snd✝) ha ∈
      filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2)))
[PROOFSTEP]
simp (config := { contextual := true }) only [mem_filter, and_self_iff, Prod.swap_prod_mk, forall_true_iff, mem_product]
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
x✝¹ x✝ : ℕ × ℕ
fst✝¹ snd✝¹ fst✝ snd✝ : ℕ
⊢ ∀ (ha : (fst✝¹, snd✝¹) ∈ filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2))))
    (hb : (fst✝, snd✝) ∈ filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))),
    (fun x x_1 => Prod.swap x) (fst✝¹, snd✝¹) ha = (fun x x_1 => Prod.swap x) (fst✝, snd✝) hb →
      (fst✝¹, snd✝¹) = (fst✝, snd✝)
[PROOFSTEP]
simp (config := { contextual := true }) only [Prod.mk.inj_iff, eq_self_iff_true, and_self_iff, Prod.swap_prod_mk,
  forall_true_iff]
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
x✝ : ℕ × ℕ
x₁ x₂ : ℕ
h : (x₁, x₂) ∈ filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2)))
⊢ ∃ ha, (fun x x_1 => Prod.swap x) (x₂, x₁) ha = (x₁, x₂)
[PROOFSTEP]
revert h
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
x✝ : ℕ × ℕ
x₁ x₂ : ℕ
⊢ (x₁, x₂) ∈ filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))) →
    ∃ ha, (fun x x_1 => Prod.swap x) (x₂, x₁) ha = (x₁, x₂)
[PROOFSTEP]
simp (config := { contextual := true }) only [mem_filter, eq_self_iff_true, and_self_iff, exists_prop_of_true,
  Prod.swap_prod_mk, forall_true_iff, mem_product]
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
⊢ ∑ a in Ico 1 (succ (p / 2)), a * q / p + ∑ a in Ico 1 (succ (q / 2)), a * p / q = p / 2 * (q / 2)
[PROOFSTEP]
have hdisj :
  Disjoint ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter fun x : ℕ × ℕ => x.2 * p ≤ x.1 * q)
    ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter fun x : ℕ × ℕ => x.1 * q ≤ x.2 * p) :=
  by
  apply disjoint_filter.2 fun x hx hpq hqp => ?_
  have hxp : x.1 < p :=
    lt_of_le_of_lt (show x.1 ≤ p / 2 by simp_all only [lt_succ_iff, mem_Ico, mem_product])
      (Nat.div_lt_self hp.1.pos (by decide))
  have : (x.1 : ZMod p) = 0 := by simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hpq hqp)
  apply_fun ZMod.val at this 
  rw [val_cast_of_lt hxp, val_zero] at this 
  simp only [this, nonpos_iff_eq_zero, mem_Ico, one_ne_zero, false_and_iff, mem_product] at hx 
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
⊢ Disjoint (filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
    (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
[PROOFSTEP]
apply disjoint_filter.2 fun x hx hpq hqp => ?_
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
x : ℕ × ℕ
hx : x ∈ Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
hpq : x.snd * p ≤ x.fst * q
hqp : x.fst * q ≤ x.snd * p
⊢ False
[PROOFSTEP]
have hxp : x.1 < p :=
  lt_of_le_of_lt (show x.1 ≤ p / 2 by simp_all only [lt_succ_iff, mem_Ico, mem_product])
    (Nat.div_lt_self hp.1.pos (by decide))
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
x : ℕ × ℕ
hx : x ∈ Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
hpq : x.snd * p ≤ x.fst * q
hqp : x.fst * q ≤ x.snd * p
⊢ x.fst ≤ p / 2
[PROOFSTEP]
simp_all only [lt_succ_iff, mem_Ico, mem_product]
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
x : ℕ × ℕ
hx : x ∈ Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
hpq : x.snd * p ≤ x.fst * q
hqp : x.fst * q ≤ x.snd * p
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
x : ℕ × ℕ
hx : x ∈ Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
hpq : x.snd * p ≤ x.fst * q
hqp : x.fst * q ≤ x.snd * p
hxp : x.fst < p
⊢ False
[PROOFSTEP]
have : (x.1 : ZMod p) = 0 := by simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hpq hqp)
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
x : ℕ × ℕ
hx : x ∈ Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
hpq : x.snd * p ≤ x.fst * q
hqp : x.fst * q ≤ x.snd * p
hxp : x.fst < p
⊢ ↑x.fst = 0
[PROOFSTEP]
simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hpq hqp)
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
x : ℕ × ℕ
hx : x ∈ Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
hpq : x.snd * p ≤ x.fst * q
hqp : x.fst * q ≤ x.snd * p
hxp : x.fst < p
this : ↑x.fst = 0
⊢ False
[PROOFSTEP]
apply_fun ZMod.val at this 
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
x : ℕ × ℕ
hx : x ∈ Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
hpq : x.snd * p ≤ x.fst * q
hqp : x.fst * q ≤ x.snd * p
hxp : x.fst < p
this : val ↑x.fst = val 0
⊢ False
[PROOFSTEP]
rw [val_cast_of_lt hxp, val_zero] at this 
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
x : ℕ × ℕ
hx : x ∈ Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
hpq : x.snd * p ≤ x.fst * q
hqp : x.fst * q ≤ x.snd * p
hxp : x.fst < p
this : x.fst = 0
⊢ False
[PROOFSTEP]
simp only [this, nonpos_iff_eq_zero, mem_Ico, one_ne_zero, false_and_iff, mem_product] at hx 
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
hdisj :
  Disjoint (filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
    (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
⊢ ∑ a in Ico 1 (succ (p / 2)), a * q / p + ∑ a in Ico 1 (succ (q / 2)), a * p / q = p / 2 * (q / 2)
[PROOFSTEP]
have hunion :
  (((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter fun x : ℕ × ℕ => x.2 * p ≤ x.1 * q) ∪
      (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter fun x : ℕ × ℕ => x.1 * q ≤ x.2 * p) =
    Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ :=
  Finset.ext fun x => by
    have := le_total (x.2 * p) (x.1 * q)
    simp only [mem_union, mem_filter, mem_Ico, mem_product]
    tauto
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
hdisj :
  Disjoint (filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
    (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
x : ℕ × ℕ
⊢ x ∈
      filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))) ∪
        filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))) ↔
    x ∈ Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
[PROOFSTEP]
have := le_total (x.2 * p) (x.1 * q)
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
hdisj :
  Disjoint (filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
    (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
x : ℕ × ℕ
this : x.snd * p ≤ x.fst * q ∨ x.fst * q ≤ x.snd * p
⊢ x ∈
      filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))) ∪
        filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))) ↔
    x ∈ Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
[PROOFSTEP]
simp only [mem_union, mem_filter, mem_Ico, mem_product]
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
hdisj :
  Disjoint (filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
    (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
x : ℕ × ℕ
this : x.snd * p ≤ x.fst * q ∨ x.fst * q ≤ x.snd * p
⊢ ((1 ≤ x.fst ∧ x.fst < succ (p / 2)) ∧ 1 ≤ x.snd ∧ x.snd < succ (q / 2)) ∧ x.snd * p ≤ x.fst * q ∨
      ((1 ≤ x.fst ∧ x.fst < succ (p / 2)) ∧ 1 ≤ x.snd ∧ x.snd < succ (q / 2)) ∧ x.fst * q ≤ x.snd * p ↔
    (1 ≤ x.fst ∧ x.fst < succ (p / 2)) ∧ 1 ≤ x.snd ∧ x.snd < succ (q / 2)
[PROOFSTEP]
tauto
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
hdisj :
  Disjoint (filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
    (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
hunion :
  filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))) ∪
      filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))) =
    Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
⊢ ∑ a in Ico 1 (succ (p / 2)), a * q / p + ∑ a in Ico 1 (succ (q / 2)), a * p / q = p / 2 * (q / 2)
[PROOFSTEP]
rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_disjoint_union hdisj, hunion, card_product]
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  Finset.card (filter (fun x => x.snd * q ≤ x.fst * p) (Ico 1 (succ (q / 2)) ×ˢ Ico 1 (succ (p / 2)))) =
    Finset.card (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
hdisj :
  Disjoint (filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
    (filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))))
hunion :
  filter (fun x => x.snd * p ≤ x.fst * q) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))) ∪
      filter (fun x => x.fst * q ≤ x.snd * p) (Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))) =
    Ico 1 (succ (p / 2)) ×ˢ Ico 1 (succ (q / 2))
⊢ Finset.card (Ico 1 (succ (p / 2))) * Finset.card (Ico 1 (succ (q / 2))) = p / 2 * (q / 2)
[PROOFSTEP]
simp only [card_Ico, tsub_zero, succ_sub_succ_eq_sub]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
⊢ legendreSym p ↑a = (-1) ^ ∑ x in Ico 1 (succ (p / 2)), x * a / p
[PROOFSTEP]
haveI hp' : Fact (p % 2 = 1) := ⟨Nat.Prime.mod_two_eq_one_iff_ne_two.mpr hp⟩
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
⊢ legendreSym p ↑a = (-1) ^ ∑ x in Ico 1 (succ (p / 2)), x * a / p
[PROOFSTEP]
have ha0' : ((a : ℤ) : ZMod p) ≠ 0 := by norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
⊢ ↑↑a ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ legendreSym p ↑a = (-1) ^ ∑ x in Ico 1 (succ (p / 2)), x * a / p
[PROOFSTEP]
rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
  (by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)), show _ = _ from eisenstein_lemma_aux p ha1 ha0]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ ↑↑a = ↑a
[PROOFSTEP]
norm_cast
