[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


[GOAL]
p : ℕ
⊢ padicValNat p 0 = 0
[PROOFSTEP]
simp [padicValNat]
[GOAL]
p : ℕ
⊢ padicValNat p 1 = 0
[PROOFSTEP]
unfold padicValNat
[GOAL]
p : ℕ
⊢ (if h : p ≠ 1 ∧ 0 < 1 then Part.get (multiplicity p 1) (_ : multiplicity.Finite p 1) else 0) = 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
p : ℕ
h✝ : p ≠ 1 ∧ 0 < 1
⊢ Part.get (multiplicity p 1) (_ : multiplicity.Finite p 1) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
p : ℕ
h✝ : ¬(p ≠ 1 ∧ 0 < 1)
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : 1 < p
⊢ padicValNat p p = 1
[PROOFSTEP]
have neq_one : ¬p = 1 ↔ True := iff_of_true hp.ne' trivial
[GOAL]
p : ℕ
hp : 1 < p
neq_one : ¬p = 1 ↔ True
⊢ padicValNat p p = 1
[PROOFSTEP]
have eq_zero_false : p = 0 ↔ False := iff_false_intro (zero_lt_one.trans hp).ne'
[GOAL]
p : ℕ
hp : 1 < p
neq_one : ¬p = 1 ↔ True
eq_zero_false : p = 0 ↔ False
⊢ padicValNat p p = 1
[PROOFSTEP]
simp [padicValNat, neq_one, eq_zero_false]
[GOAL]
p n : ℕ
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
[PROOFSTEP]
simp only [padicValNat, dite_eq_right_iff, PartENat.get_eq_iff_eq_coe, Nat.cast_zero, multiplicity_eq_zero, and_imp,
  pos_iff_ne_zero, Ne.def, ← or_iff_not_imp_left]
[GOAL]
p✝ p n : ℕ
hp : 1 < p
hn : 0 < n
⊢ ↑(maxPowDiv p n) = multiplicity p n
[PROOFSTEP]
apply multiplicity.unique <| pow_dvd p n
[GOAL]
p✝ p n : ℕ
hp : 1 < p
hn : 0 < n
⊢ ¬p ^ (maxPowDiv p n + 1) ∣ n
[PROOFSTEP]
intro h
[GOAL]
p✝ p n : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ (maxPowDiv p n + 1) ∣ n
⊢ False
[PROOFSTEP]
apply Nat.not_lt.mpr <| le_of_dvd hp hn h
[GOAL]
p✝ p n : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ (maxPowDiv p n + 1) ∣ n
⊢ maxPowDiv p n < maxPowDiv p n + 1
[PROOFSTEP]
simp
[GOAL]
p✝ p n : ℕ
hp : 1 < p
hn : 0 < n
h : multiplicity.Finite p n
⊢ maxPowDiv p n = Part.get (multiplicity p n) h
[PROOFSTEP]
rw [PartENat.get_eq_iff_eq_coe.mpr]
[GOAL]
p✝ p n : ℕ
hp : 1 < p
hn : 0 < n
h : multiplicity.Finite p n
⊢ multiplicity p n = ↑(maxPowDiv p n)
[PROOFSTEP]
apply maxPowDiv_eq_multiplicity hp hn |>.symm
[GOAL]
p : ℕ
⊢ padicValNat = maxPowDiv
[PROOFSTEP]
ext p n
[GOAL]
case h.h
p✝ p n : ℕ
⊢ padicValNat p n = maxPowDiv p n
[PROOFSTEP]
by_cases (1 < p ∧ 0 < n)
[GOAL]
case h.h
p✝ p n : ℕ
⊢ padicValNat p n = maxPowDiv p n
[PROOFSTEP]
by_cases (1 < p ∧ 0 < n)
[GOAL]
case pos
p✝ p n : ℕ
h : 1 < p ∧ 0 < n
⊢ padicValNat p n = maxPowDiv p n
[PROOFSTEP]
dsimp [padicValNat]
[GOAL]
case pos
p✝ p n : ℕ
h : 1 < p ∧ 0 < n
⊢ (if h : ¬p = 1 ∧ 0 < n then Part.get (multiplicity p n) (_ : multiplicity.Finite p n) else 0) = maxPowDiv p n
[PROOFSTEP]
rw [dif_pos ⟨Nat.ne_of_gt h.1, h.2⟩, maxPowDiv_eq_multiplicity_get h.1 h.2]
[GOAL]
case neg
p✝ p n : ℕ
h : ¬(1 < p ∧ 0 < n)
⊢ padicValNat p n = maxPowDiv p n
[PROOFSTEP]
simp only [not_and_or, not_gt_eq, le_zero_iff] at h
[GOAL]
case neg
p✝ p n : ℕ
h : p ≤ 1 ∨ n = 0
⊢ padicValNat p n = maxPowDiv p n
[PROOFSTEP]
apply h.elim
[GOAL]
case neg.left
p✝ p n : ℕ
h : p ≤ 1 ∨ n = 0
⊢ p ≤ 1 → padicValNat p n = maxPowDiv p n
[PROOFSTEP]
intro h
[GOAL]
case neg.left
p✝ p n : ℕ
h✝ : p ≤ 1 ∨ n = 0
h : p ≤ 1
⊢ padicValNat p n = maxPowDiv p n
[PROOFSTEP]
interval_cases p
[GOAL]
case neg.left.«0»
p✝ p n : ℕ
h✝ : 0 ≤ 1 ∨ n = 0
h : 0 ≤ 1
⊢ padicValNat 0 n = maxPowDiv 0 n
[PROOFSTEP]
simp [Classical.em]
[GOAL]
case neg.left.«1»
p✝ p n : ℕ
h✝ : 1 ≤ 1 ∨ n = 0
h : 1 ≤ 1
⊢ padicValNat 1 n = maxPowDiv 1 n
[PROOFSTEP]
dsimp [padicValNat, maxPowDiv]
[GOAL]
case neg.left.«1»
p✝ p n : ℕ
h✝ : 1 ≤ 1 ∨ n = 0
h : 1 ≤ 1
⊢ (if h : ¬1 = 1 ∧ 0 < n then Part.get (multiplicity 1 n) (_ : multiplicity.Finite 1 n) else 0) = go 0 1 n
[PROOFSTEP]
rw [go_eq, if_neg, dif_neg]
[GOAL]
case neg.left.«1».hnc
p✝ p n : ℕ
h✝ : 1 ≤ 1 ∨ n = 0
h : 1 ≤ 1
⊢ ¬(¬1 = 1 ∧ 0 < n)
[PROOFSTEP]
simp
[GOAL]
case neg.left.«1».hnc
p✝ p n : ℕ
h✝ : 1 ≤ 1 ∨ n = 0
h : 1 ≤ 1
⊢ ¬(1 < 1 ∧ 0 < n ∧ n % 1 = 0)
[PROOFSTEP]
simp
[GOAL]
case neg.right
p✝ p n : ℕ
h : p ≤ 1 ∨ n = 0
⊢ n = 0 → padicValNat p n = maxPowDiv p n
[PROOFSTEP]
intro h
[GOAL]
case neg.right
p✝ p n : ℕ
h✝ : p ≤ 1 ∨ n = 0
h : n = 0
⊢ padicValNat p n = maxPowDiv p n
[PROOFSTEP]
simp [h]
[GOAL]
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ (multiplicity (↑p) z).Dom
[PROOFSTEP]
apply multiplicity.finite_int_iff.2
[GOAL]
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ Int.natAbs ↑p ≠ 1 ∧ z ≠ 0
[PROOFSTEP]
simp [hp, hz]
[GOAL]
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ padicValInt p z = Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z)
[PROOFSTEP]
rw [padicValInt, padicValNat, dif_pos (And.intro hp (Int.natAbs_pos.mpr hz))]
[GOAL]
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ Part.get (multiplicity p (Int.natAbs z)) (_ : multiplicity.Finite p (Int.natAbs z)) =
    Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z)
[PROOFSTEP]
simp only [multiplicity.Int.natAbs p z]
[GOAL]
p : ℕ
⊢ padicValInt p 0 = 0
[PROOFSTEP]
simp [padicValInt]
[GOAL]
p : ℕ
⊢ padicValInt p 1 = 0
[PROOFSTEP]
simp [padicValInt]
[GOAL]
p n : ℕ
⊢ padicValInt p ↑n = padicValNat p n
[PROOFSTEP]
simp [padicValInt]
[GOAL]
p : ℕ
hp : 1 < p
⊢ padicValInt p ↑p = 1
[PROOFSTEP]
simp [padicValNat.self hp]
[GOAL]
p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ padicValInt p z = 0
[PROOFSTEP]
rw [padicValInt, padicValNat]
[GOAL]
p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ (if h : p ≠ 1 ∧ 0 < Int.natAbs z then
      Part.get (multiplicity p (Int.natAbs z)) (_ : multiplicity.Finite p (Int.natAbs z))
    else 0) =
    0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
p : ℕ
z : ℤ
h : ¬↑p ∣ z
h✝ : p ≠ 1 ∧ 0 < Int.natAbs z
⊢ Part.get (multiplicity p (Int.natAbs z)) (_ : multiplicity.Finite p (Int.natAbs z)) = 0
[PROOFSTEP]
simp [multiplicity.Int.natAbs, multiplicity_eq_zero.2 h]
[GOAL]
case neg
p : ℕ
z : ℤ
h : ¬↑p ∣ z
h✝ : ¬(p ≠ 1 ∧ 0 < Int.natAbs z)
⊢ 0 = 0
[PROOFSTEP]
simp [multiplicity.Int.natAbs, multiplicity_eq_zero.2 h]
[GOAL]
p : ℕ
q : ℚ
⊢ padicValRat p (-q) = padicValRat p q
[PROOFSTEP]
simp [padicValRat, padicValInt]
[GOAL]
p : ℕ
⊢ padicValRat p 0 = 0
[PROOFSTEP]
simp [padicValRat]
[GOAL]
p : ℕ
⊢ padicValRat p 1 = 0
[PROOFSTEP]
simp [padicValRat]
[GOAL]
p : ℕ
z : ℤ
⊢ padicValRat p ↑z = ↑(padicValInt p z)
[PROOFSTEP]
simp [padicValRat]
[GOAL]
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ padicValRat p ↑z = ↑(Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z))
[PROOFSTEP]
rw [of_int, padicValInt.of_ne_one_ne_zero hp hz]
[GOAL]
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ (multiplicity p q.den).Dom
[PROOFSTEP]
rw [← finite_iff_dom, finite_nat_iff]
[GOAL]
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ p ≠ 1 ∧ 0 < q.den
[PROOFSTEP]
exact ⟨hp, q.pos⟩
[GOAL]
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ padicValRat p q =
    ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
      ↑(Part.get (multiplicity p q.den) (_ : (multiplicity p q.den).Dom))
[PROOFSTEP]
rw [padicValRat, padicValInt.of_ne_one_ne_zero hp, padicValNat, dif_pos]
[GOAL]
case hc
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ p ≠ 1 ∧ 0 < q.den
[PROOFSTEP]
exact ⟨hp, q.pos⟩
[GOAL]
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ q.num ≠ 0
[PROOFSTEP]
exact Rat.num_ne_zero_of_ne_zero hq
[GOAL]
p n : ℕ
⊢ padicValRat p ↑n = ↑(padicValNat p n)
[PROOFSTEP]
simp [padicValRat]
[GOAL]
p : ℕ
hp : 1 < p
⊢ padicValRat p ↑p = 1
[PROOFSTEP]
simp [hp]
[GOAL]
p n : ℕ
⊢ 0 ≤ padicValRat p ↑n
[PROOFSTEP]
simp
[GOAL]
p n : ℕ
⊢ ↑(padicValNat p n) = padicValRat p ↑n
[PROOFSTEP]
simp
[GOAL]
p n : ℕ
hp : p ≠ 1
hn : 0 < n
⊢ ↑(padicValNat p n) = multiplicity p n
[PROOFSTEP]
simp [padicValNat, hp, hn]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ padicValNat p p = 1
[PROOFSTEP]
rw [padicValNat_def (@Fact.out p.Prime).pos]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Part.get (multiplicity p p) (_ : multiplicity.Finite p p) = 1
[PROOFSTEP]
simp
[GOAL]
p n : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
div : p ∣ n
⊢ 1 ≤ padicValNat p n
[PROOFSTEP]
rwa [← PartENat.coe_le_coe, padicValNat_def' hp.out.ne_one hn, ← pow_dvd_iff_le_multiplicity, pow_one]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ multiplicity.Finite (↑p) a ↔ a ≠ 0
[PROOFSTEP]
simp [finite_int_iff, hp.1.ne_one]
[GOAL]
p✝ : ℕ
hp✝ : Fact (Nat.Prime p✝)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hn : n = 0
⊢ False
[PROOFSTEP]
simp_all
[GOAL]
p✝ : ℕ
hp✝ : Fact (Nat.Prime p✝)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d = 0
⊢ False
[PROOFSTEP]
simp_all
[GOAL]
p✝ : ℕ
hp✝ : Fact (Nat.Prime p✝)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
⊢ padicValRat p q =
    ↑(Part.get (multiplicity (↑p) n) (_ : multiplicity.Finite (↑p) n)) -
      ↑(Part.get (multiplicity (↑p) d) (_ : multiplicity.Finite (↑p) d))
[PROOFSTEP]
have hd : d ≠ 0 := Rat.mk_denom_ne_zero_of_ne_zero hqz qdf
[GOAL]
p✝ : ℕ
hp✝ : Fact (Nat.Prime p✝)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
⊢ padicValRat p q =
    ↑(Part.get (multiplicity (↑p) n) (_ : multiplicity.Finite (↑p) n)) -
      ↑(Part.get (multiplicity (↑p) d) (_ : multiplicity.Finite (↑p) d))
[PROOFSTEP]
let ⟨c, hc1, hc2⟩ := Rat.num_den_mk hd qdf
[GOAL]
p✝ : ℕ
hp✝ : Fact (Nat.Prime p✝)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ padicValRat p q =
    ↑(Part.get (multiplicity (↑p) n) (_ : multiplicity.Finite (↑p) n)) -
      ↑(Part.get (multiplicity (↑p) d) (_ : multiplicity.Finite (↑p) d))
[PROOFSTEP]
rw [padicValRat.multiplicity_sub_multiplicity hp.1.ne_one hqz]
[GOAL]
p✝ : ℕ
hp✝ : Fact (Nat.Prime p✝)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
      ↑(Part.get (multiplicity p q.den) (_ : (multiplicity p q.den).Dom)) =
    ↑(Part.get (multiplicity (↑p) n) (_ : multiplicity.Finite (↑p) n)) -
      ↑(Part.get (multiplicity (↑p) d) (_ : multiplicity.Finite (↑p) d))
[PROOFSTEP]
simp only [Nat.isUnit_iff, hc1, hc2]
[GOAL]
p✝ : ℕ
hp✝ : Fact (Nat.Prime p✝)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
      ↑(Part.get (multiplicity p q.den) (_ : (multiplicity p q.den).Dom)) =
    ↑(Part.get (multiplicity (↑p) (c * q.num)) (_ : (multiplicity (↑p) (c * q.num)).Dom)) -
      ↑(Part.get (multiplicity (↑p) (c * ↑q.den)) (_ : (multiplicity (↑p) (c * ↑q.den)).Dom))
[PROOFSTEP]
rw [multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1), multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1)]
[GOAL]
p✝ : ℕ
hp✝ : Fact (Nat.Prime p✝)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
      ↑(Part.get (multiplicity p q.den) (_ : (multiplicity p q.den).Dom)) =
    ↑(Part.get (multiplicity (↑p) c) (_ : multiplicity.Finite (↑p) c) +
          Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
      ↑(Part.get (multiplicity (↑p) c) (_ : multiplicity.Finite (↑p) c) +
          Part.get (multiplicity ↑p ↑q.den) (_ : multiplicity.Finite ↑p ↑q.den))
[PROOFSTEP]
rw [Nat.cast_add, Nat.cast_add]
[GOAL]
p✝ : ℕ
hp✝ : Fact (Nat.Prime p✝)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
      ↑(Part.get (multiplicity p q.den) (_ : (multiplicity p q.den).Dom)) =
    ↑(Part.get (multiplicity (↑p) c) (_ : multiplicity.Finite (↑p) c)) +
        ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
      (↑(Part.get (multiplicity (↑p) c) (_ : multiplicity.Finite (↑p) c)) +
        ↑(Part.get (multiplicity ↑p ↑q.den) (_ : multiplicity.Finite ↑p ↑q.den)))
[PROOFSTEP]
simp_rw [Int.coe_nat_multiplicity p q.den]
[GOAL]
p✝ : ℕ
hp✝ : Fact (Nat.Prime p✝)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
      ↑(Part.get (multiplicity p q.den) (_ : (multiplicity p q.den).Dom)) =
    ↑(Part.get (multiplicity (↑p) c) (_ : multiplicity.Finite (↑p) c)) +
        ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
      (↑(Part.get (multiplicity (↑p) c) (_ : multiplicity.Finite (↑p) c)) +
        ↑(Part.get (multiplicity p q.den) (_ : (multiplicity p q.den).Dom)))
[PROOFSTEP]
ring
  -- Porting note: was
    -- simp only [hc1, hc2, multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1),
    --   hp.1.ne_one, hqz, pos_iff_ne_zero, Int.coe_nat_multiplicity p q.den
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
[PROOFSTEP]
have : q * r = q.num * r.num /. (q.den * r.den) := by rw_mod_cast [Rat.mul_num_den]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ q * r = q.num * r.num /. (↑q.den * ↑r.den)
[PROOFSTEP]
rw_mod_cast [Rat.mul_num_den]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
[PROOFSTEP]
have hq' : q.num /. q.den ≠ 0 := by rwa [Rat.num_den]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
⊢ q.num /. ↑q.den ≠ 0
[PROOFSTEP]
rwa [Rat.num_den]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
[PROOFSTEP]
have hr' : r.num /. r.den ≠ 0 := by rwa [Rat.num_den]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
⊢ r.num /. ↑r.den ≠ 0
[PROOFSTEP]
rwa [Rat.num_den]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
[PROOFSTEP]
have hp' : Prime (p : ℤ) := Nat.prime_iff_prime_int.1 hp.1
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
[PROOFSTEP]
rw [padicValRat.defn p (mul_ne_zero hq hr) this]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(Part.get (multiplicity (↑p) (q.num * r.num)) (_ : multiplicity.Finite (↑p) (q.num * r.num))) -
      ↑(Part.get (multiplicity (↑p) (↑q.den * ↑r.den)) (_ : multiplicity.Finite (↑p) (↑q.den * ↑r.den))) =
    padicValRat p q + padicValRat p r
[PROOFSTEP]
conv_rhs => rw [← @Rat.num_den q, padicValRat.defn p hq', ← @Rat.num_den r, padicValRat.defn p hr']
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
| padicValRat p q + padicValRat p r
[PROOFSTEP]
rw [← @Rat.num_den q, padicValRat.defn p hq', ← @Rat.num_den r, padicValRat.defn p hr']
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
| padicValRat p q + padicValRat p r
[PROOFSTEP]
rw [← @Rat.num_den q, padicValRat.defn p hq', ← @Rat.num_den r, padicValRat.defn p hr']
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
| padicValRat p q + padicValRat p r
[PROOFSTEP]
rw [← @Rat.num_den q, padicValRat.defn p hq', ← @Rat.num_den r, padicValRat.defn p hr']
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(Part.get (multiplicity (↑p) (q.num * r.num)) (_ : multiplicity.Finite (↑p) (q.num * r.num))) -
      ↑(Part.get (multiplicity (↑p) (↑q.den * ↑r.den)) (_ : multiplicity.Finite (↑p) (↑q.den * ↑r.den))) =
    ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
        ↑(Part.get (multiplicity ↑p ↑q.den) (_ : multiplicity.Finite ↑p ↑q.den)) +
      (↑(Part.get (multiplicity (↑p) r.num) (_ : multiplicity.Finite (↑p) r.num)) -
        ↑(Part.get (multiplicity ↑p ↑r.den) (_ : multiplicity.Finite ↑p ↑r.den)))
[PROOFSTEP]
rw [multiplicity.mul' hp', multiplicity.mul' hp', Nat.cast_add, Nat.cast_add]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) +
        ↑(Part.get (multiplicity (↑p) r.num) (_ : multiplicity.Finite (↑p) r.num)) -
      (↑(Part.get (multiplicity ↑p ↑q.den) (_ : multiplicity.Finite ↑p ↑q.den)) +
        ↑(Part.get (multiplicity ↑p ↑r.den) (_ : multiplicity.Finite ↑p ↑r.den))) =
    ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
        ↑(Part.get (multiplicity ↑p ↑q.den) (_ : multiplicity.Finite ↑p ↑q.den)) +
      (↑(Part.get (multiplicity (↑p) r.num) (_ : multiplicity.Finite (↑p) r.num)) -
        ↑(Part.get (multiplicity ↑p ↑r.den) (_ : multiplicity.Finite ↑p ↑r.den)))
[PROOFSTEP]
ring
  -- Porting note: was
    -- simp [add_comm, add_left_comm, sub_eq_add_neg]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
k : ℕ
⊢ padicValRat p (q ^ k) = ↑k * padicValRat p q
[PROOFSTEP]
induction k
[GOAL]
case zero
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicValRat p (q ^ zero) = ↑zero * padicValRat p q
[PROOFSTEP]
simp [*, padicValRat.mul hq (pow_ne_zero _ hq), _root_.pow_succ, add_mul, add_comm]
[GOAL]
case succ
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
n✝ : ℕ
n_ih✝ : padicValRat p (q ^ n✝) = ↑n✝ * padicValRat p q
⊢ padicValRat p (q ^ succ n✝) = ↑(succ n✝) * padicValRat p q
[PROOFSTEP]
simp [*, padicValRat.mul hq (pow_ne_zero _ hq), _root_.pow_succ, add_mul, add_comm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ padicValRat p q⁻¹ = -padicValRat p q
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q
[PROOFSTEP]
simp [hq]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q
[PROOFSTEP]
rw [eq_neg_iff_add_eq_zero, ← padicValRat.mul (inv_ne_zero hq) hq, inv_mul_cancel hq, padicValRat.one]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ padicValRat p (q / r) = padicValRat p q - padicValRat p r
[PROOFSTEP]
rw [div_eq_mul_inv, padicValRat.mul hq (inv_ne_zero hr), padicValRat.inv r, sub_eq_add_neg]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
[PROOFSTEP]
have hf1 : Finite (p : ℤ) (n₁ * d₂) := finite_int_prime_iff.2 (mul_ne_zero hn₁ hd₂)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : multiplicity.Finite (↑p) (n₁ * d₂)
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
[PROOFSTEP]
have hf2 : Finite (p : ℤ) (n₂ * d₁) := finite_int_prime_iff.2 (mul_ne_zero hn₂ hd₁)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : multiplicity.Finite (↑p) (n₁ * d₂)
hf2 : multiplicity.Finite (↑p) (n₂ * d₁)
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
[PROOFSTEP]
conv =>
  lhs
  rw [padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₁ hd₁) rfl,
    padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl, sub_le_iff_le_add', ← add_sub_assoc,
    _root_.le_sub_iff_add_le]
  norm_cast
  rw [← multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1) hf1, add_comm, ←
    multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1) hf2, PartENat.get_le_get, multiplicity_le_multiplicity_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : multiplicity.Finite (↑p) (n₁ * d₂)
hf2 : multiplicity.Finite (↑p) (n₂ * d₁)
| padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
[PROOFSTEP]
  lhs
  rw [padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₁ hd₁) rfl,
    padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl, sub_le_iff_le_add', ← add_sub_assoc,
    _root_.le_sub_iff_add_le]
  norm_cast
  rw [← multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1) hf1, add_comm, ←
    multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1) hf2, PartENat.get_le_get, multiplicity_le_multiplicity_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : multiplicity.Finite (↑p) (n₁ * d₂)
hf2 : multiplicity.Finite (↑p) (n₂ * d₁)
| padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
[PROOFSTEP]
  lhs
  rw [padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₁ hd₁) rfl,
    padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl, sub_le_iff_le_add', ← add_sub_assoc,
    _root_.le_sub_iff_add_le]
  norm_cast
  rw [← multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1) hf1, add_comm, ←
    multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1) hf2, PartENat.get_le_get, multiplicity_le_multiplicity_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : multiplicity.Finite (↑p) (n₁ * d₂)
hf2 : multiplicity.Finite (↑p) (n₂ * d₁)
| padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
[PROOFSTEP]
lhs
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : multiplicity.Finite (↑p) (n₁ * d₂)
hf2 : multiplicity.Finite (↑p) (n₂ * d₁)
| padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂)
[PROOFSTEP]
rw [padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₁ hd₁) rfl,
  padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl, sub_le_iff_le_add', ← add_sub_assoc,
  _root_.le_sub_iff_add_le]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : multiplicity.Finite (↑p) (n₁ * d₂)
hf2 : multiplicity.Finite (↑p) (n₂ * d₁)
| ↑(Part.get (multiplicity (↑p) n₁) (_ : multiplicity.Finite (↑p) n₁)) +
      ↑(Part.get (multiplicity (↑p) d₂) (_ : multiplicity.Finite (↑p) d₂)) ≤
    ↑(Part.get (multiplicity (↑p) d₁) (_ : multiplicity.Finite (↑p) d₁)) +
      ↑(Part.get (multiplicity (↑p) n₂) (_ : multiplicity.Finite (↑p) n₂))
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : multiplicity.Finite (↑p) (n₁ * d₂)
hf2 : multiplicity.Finite (↑p) (n₂ * d₁)
| Part.get (multiplicity (↑p) n₁) (_ : multiplicity.Finite (↑p) n₁) +
      Part.get (multiplicity (↑p) d₂) (_ : multiplicity.Finite (↑p) d₂) ≤
    Part.get (multiplicity (↑p) d₁) (_ : multiplicity.Finite (↑p) d₁) +
      Part.get (multiplicity (↑p) n₂) (_ : multiplicity.Finite (↑p) n₂)
[PROOFSTEP]
rw [← multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1) hf1, add_comm, ←
  multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1) hf2, PartENat.get_le_get, multiplicity_le_multiplicity_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : q = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
simpa [hq] using h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : r = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
simp [hr]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
have hqn : q.num ≠ 0 := Rat.num_ne_zero_of_ne_zero hq
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
have hqd : (q.den : ℤ) ≠ 0 := by exact_mod_cast Rat.den_nz _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
⊢ ↑q.den ≠ 0
[PROOFSTEP]
exact_mod_cast Rat.den_nz _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
have hrn : r.num ≠ 0 := Rat.num_ne_zero_of_ne_zero hr
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
have hrd : (r.den : ℤ) ≠ 0 := by exact_mod_cast Rat.den_nz _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
⊢ ↑r.den ≠ 0
[PROOFSTEP]
exact_mod_cast Rat.den_nz _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
have hqreq : q + r = (q.num * r.den + q.den * r.num) /. (q.den * r.den) := Rat.add_num_den _ _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
have hqrd : q.num * r.den + q.den * r.num ≠ 0 := Rat.mk_num_ne_zero_of_ne_zero hqr hqreq
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
conv_lhs => rw [← @Rat.num_den q]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
| padicValRat p q
[PROOFSTEP]
rw [← @Rat.num_den q]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
| padicValRat p q
[PROOFSTEP]
rw [← @Rat.num_den q]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
| padicValRat p q
[PROOFSTEP]
rw [← @Rat.num_den q]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p (q.num /. ↑q.den) ≤ padicValRat p (q + r)
[PROOFSTEP]
rw [hqreq, padicValRat_le_padicValRat_iff hqn hqrd hqd (mul_ne_zero hqd hrd), ← multiplicity_le_multiplicity_iff,
  mul_left_comm, multiplicity.mul (Nat.prime_iff_prime_int.1 hp.1), add_mul]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤
    multiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
[PROOFSTEP]
rw [← @Rat.num_den q, ← @Rat.num_den r, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
  multiplicity_le_multiplicity_iff] at h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h✝ : ∀ (n : ℕ), ↑p ^ n ∣ q.num * ↑r.den → ↑p ^ n ∣ r.num * ↑q.den
h : multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤
    multiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
[PROOFSTEP]
calc
  _ ≤ min (multiplicity (↑p) (q.num * r.den * q.den)) (multiplicity (↑p) (↑q.den * r.num * ↑q.den)) :=
    le_min (by rw [@multiplicity.mul _ _ _ _ (_ * _) _ (Nat.prime_iff_prime_int.1 hp.1), add_comm])
      (by
        rw [mul_assoc, @multiplicity.mul _ _ _ _ (q.den : ℤ) (_ * _) (Nat.prime_iff_prime_int.1 hp.1)]
        exact add_le_add_left h _)
  _ ≤ _ := min_le_multiplicity_add
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h✝ : ∀ (n : ℕ), ↑p ^ n ∣ q.num * ↑r.den → ↑p ^ n ∣ r.num * ↑q.den
h : multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (q.num * ↑r.den * ↑q.den)
[PROOFSTEP]
rw [@multiplicity.mul _ _ _ _ (_ * _) _ (Nat.prime_iff_prime_int.1 hp.1), add_comm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h✝ : ∀ (n : ℕ), ↑p ^ n ∣ q.num * ↑r.den → ↑p ^ n ∣ r.num * ↑q.den
h : multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (↑q.den * r.num * ↑q.den)
[PROOFSTEP]
rw [mul_assoc, @multiplicity.mul _ _ _ _ (q.den : ℤ) (_ * _) (Nat.prime_iff_prime_int.1 hp.1)]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h✝ : ∀ (n : ℕ), ↑p ^ n ∣ q.num * ↑r.den → ↑p ^ n ∣ r.num * ↑q.den
h : multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤
    multiplicity ↑p ↑q.den + multiplicity (↑p) (r.num * ↑q.den)
[PROOFSTEP]
exact add_le_add_left h _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
[PROOFSTEP]
rw [min_eq_left h]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
exact le_padicValRat_add_of_le hqr h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
[PROOFSTEP]
rw [min_eq_right h, add_comm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ padicValRat p r ≤ padicValRat p (r + q)
[PROOFSTEP]
exact le_padicValRat_add_of_le (by rwa [add_comm]) h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ r + q ≠ 0
[PROOFSTEP]
rwa [add_comm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0 : ∑ i in Finset.range n, F i ≠ 0
⊢ 0 < padicValRat p (∑ i in Finset.range n, F i)
[PROOFSTEP]
induction' n with d hd
[GOAL]
case zero
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
hF : ∀ (i : ℕ), i < zero → 0 < padicValRat p (F i)
hn0 : ∑ i in Finset.range zero, F i ≠ 0
⊢ 0 < padicValRat p (∑ i in Finset.range zero, F i)
[PROOFSTEP]
exact False.elim (hn0 rfl)
[GOAL]
case succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ i in Finset.range (succ d), F i ≠ 0
⊢ 0 < padicValRat p (∑ i in Finset.range (succ d), F i)
[PROOFSTEP]
rw [Finset.sum_range_succ] at hn0 ⊢
[GOAL]
case succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
⊢ 0 < padicValRat p (∑ x in Finset.range d, F x + F d)
[PROOFSTEP]
by_cases h : ∑ x : ℕ in Finset.range d, F x = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ∑ x in Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x in Finset.range d, F x + F d)
[PROOFSTEP]
rw [h, zero_add]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ∑ x in Finset.range d, F x = 0
⊢ 0 < padicValRat p (F d)
[PROOFSTEP]
exact hF d (lt_add_one _)
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ¬∑ x in Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x in Finset.range d, F x + F d)
[PROOFSTEP]
refine' lt_of_lt_of_le _ (min_le_padicValRat_add hn0)
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ¬∑ x in Finset.range d, F x = 0
⊢ 0 < min (padicValRat p (∑ x in Finset.range d, F x)) (padicValRat p (F d))
[PROOFSTEP]
refine' lt_min (hd (fun i hi => _) h) (hF d (lt_add_one _))
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ¬∑ x in Finset.range d, F x = 0
i : ℕ
hi : i < d
⊢ 0 < padicValRat p (F i)
[PROOFSTEP]
exact hF _ (lt_trans hi (lt_add_one _))
[GOAL]
p a b : ℕ
hp : Fact (Nat.Prime p)
⊢ a ≠ 0 → b ≠ 0 → padicValNat p (a * b) = padicValNat p a + padicValNat p b
[PROOFSTEP]
exact_mod_cast @padicValRat.mul p _ a b
[GOAL]
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
p b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ 0
⊢ padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b
[PROOFSTEP]
simp
[GOAL]
case inr
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
ha : a ≠ 0
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b
[PROOFSTEP]
obtain ⟨k, rfl⟩ := h
[GOAL]
case inr.intro
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
[PROOFSTEP]
obtain ⟨hb, hk⟩ := mul_ne_zero_iff.mp ha
[GOAL]
case inr.intro.intro
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
[PROOFSTEP]
rw [mul_comm, k.mul_div_cancel hb.bot_lt, padicValNat.mul hk hb, Nat.add_sub_cancel]
[GOAL]
p a b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ∣ b
⊢ padicValNat p (b / p) = padicValNat p b - 1
[PROOFSTEP]
rw [padicValNat.div_of_dvd dvd, padicValNat_self]
[GOAL]
p a b : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ha : a ≠ 0
⊢ padicValNat p (a ^ n) = n * padicValNat p a
[PROOFSTEP]
simpa only [← @Nat.cast_inj ℤ, push_cast] using padicValRat.pow (Nat.cast_ne_zero.mpr ha)
[GOAL]
p a b : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ padicValNat p (p ^ n) = n
[PROOFSTEP]
rw [padicValNat.pow _ (@Fact.out p.Prime).ne_zero, padicValNat_self, mul_one]
[GOAL]
p a b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ^ a ∣ b
⊢ padicValNat p (b / p ^ a) = padicValNat p b - a
[PROOFSTEP]
rw [padicValNat.div_of_dvd dvd, padicValNat.prime_pow]
[GOAL]
p a b✝ : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
cpm : coprime p m
b : ℕ
dvd : m ∣ b
⊢ padicValNat p (b / m) = padicValNat p b
[PROOFSTEP]
rw [padicValNat.div_of_dvd dvd, eq_zero_of_not_dvd (hp.out.coprime_iff_not_dvd.mp cpm), Nat.sub_zero]
[GOAL]
p n : ℕ
hp : 1 ≤ padicValNat p n
⊢ p ∣ n
[PROOFSTEP]
by_contra h
[GOAL]
p n : ℕ
hp : 1 ≤ padicValNat p n
h : ¬p ∣ n
⊢ False
[PROOFSTEP]
rw [padicValNat.eq_zero_of_not_dvd h] at hp
[GOAL]
p n : ℕ
hp : 1 ≤ 0
h : ¬p ∣ n
⊢ False
[PROOFSTEP]
exact lt_irrefl 0 (lt_of_lt_of_le zero_lt_one hp)
[GOAL]
p n : ℕ
⊢ p ^ padicValNat p n ∣ n
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
p : ℕ
⊢ p ^ padicValNat p 0 ∣ 0
[PROOFSTEP]
simp
[GOAL]
case inr
p n : ℕ
hn : n > 0
⊢ p ^ padicValNat p n ∣ n
[PROOFSTEP]
rcases eq_or_ne p 1 with (rfl | hp)
[GOAL]
case inr.inl
n : ℕ
hn : n > 0
⊢ 1 ^ padicValNat 1 n ∣ n
[PROOFSTEP]
simp
[GOAL]
case inr.inr
p n : ℕ
hn : n > 0
hp : p ≠ 1
⊢ p ^ padicValNat p n ∣ n
[PROOFSTEP]
rw [multiplicity.pow_dvd_iff_le_multiplicity, padicValNat_def']
[GOAL]
case inr.inr.hp
p n : ℕ
hn : n > 0
hp : p ≠ 1
⊢ p ≠ 1
[PROOFSTEP]
assumption
[GOAL]
case inr.inr.hn
p n : ℕ
hn : n > 0
hp : p ≠ 1
⊢ 0 < n
[PROOFSTEP]
assumption
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a n : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ n ≤ padicValNat p a
[PROOFSTEP]
rw [pow_dvd_iff_le_multiplicity, ← padicValNat_def' hp.out.ne_one ha.bot_lt, PartENat.coe_le_coe]
[GOAL]
p n : ℕ
hp : Fact (Nat.Prime p)
a : ℕ
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ p ^ n ∣ 0 ↔ 0 = 0 ∨ n ≤ padicValNat p 0
[PROOFSTEP]
exact iff_of_true (dvd_zero _) (Or.inl rfl)
[GOAL]
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
a : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
[PROOFSTEP]
rw [padicValNat_dvd_iff_le ha, or_iff_right ha]
[GOAL]
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ ¬p ^ (padicValNat p n + 1) ∣ n
[PROOFSTEP]
rw [padicValNat_dvd_iff_le hn, not_le]
[GOAL]
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ padicValNat p n < padicValNat p n + 1
[PROOFSTEP]
exact Nat.lt_succ_self _
[GOAL]
p n : ℕ
hn : n ≠ 0
⊢ Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1)) ⊆ divisors n
[PROOFSTEP]
intro t ht
[GOAL]
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1))
⊢ t ∈ divisors n
[PROOFSTEP]
simp only [exists_prop, Finset.mem_image, Finset.mem_range] at ht
[GOAL]
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : ∃ a, a < padicValNat p n + 1 ∧ p ^ a = t
⊢ t ∈ divisors n
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := ht
[GOAL]
case intro.intro
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∈ divisors n
[PROOFSTEP]
rw [Nat.mem_divisors]
[GOAL]
case intro.intro
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∣ n ∧ n ≠ 0
[PROOFSTEP]
exact ⟨(pow_dvd_pow p <| by linarith).trans pow_padicValNat_dvd, hn⟩
[GOAL]
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ k ≤ padicValNat p n
[PROOFSTEP]
linarith
[GOAL]
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ Finset.erase (divisors n) 1
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p 0)) ⊆ Finset.erase (divisors 0) 1
[PROOFSTEP]
simp
[GOAL]
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ Finset.erase (divisors n) 1
[PROOFSTEP]
intro t ht
[GOAL]
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n))
⊢ t ∈ Finset.erase (divisors n) 1
[PROOFSTEP]
simp only [exists_prop, Finset.mem_image, Finset.mem_range] at ht
[GOAL]
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : ∃ a, a < padicValNat p n ∧ p ^ (a + 1) = t
⊢ t ∈ Finset.erase (divisors n) 1
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := ht
[GOAL]
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ∈ Finset.erase (divisors n) 1
[PROOFSTEP]
rw [Finset.mem_erase, Nat.mem_divisors]
[GOAL]
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∣ n ∧ n ≠ 0
[PROOFSTEP]
refine' ⟨_, (pow_dvd_pow p <| succ_le_iff.2 hk).trans pow_padicValNat_dvd, hn⟩
[GOAL]
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1
[PROOFSTEP]
exact (Nat.one_lt_pow _ _ k.succ_pos hp.out.one_lt).ne'
[GOAL]
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * n)! = padicValNat p n ! + n
[PROOFSTEP]
refine' PartENat.natCast_inj.mp _
[GOAL]
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑(padicValNat p (p * n)!) = ↑(padicValNat p n ! + n)
[PROOFSTEP]
rw [padicValNat_def' (Nat.Prime.ne_one hp.out) <| factorial_pos (p * n), Nat.cast_add,
  padicValNat_def' (Nat.Prime.ne_one hp.out) <| factorial_pos n]
[GOAL]
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ multiplicity p (p * n)! = multiplicity p n ! + ↑n
[PROOFSTEP]
exact Prime.multiplicity_factorial_mul hp.out
[GOAL]
p n m : ℕ
hp : Fact (Nat.Prime p)
h : n < p
⊢ padicValNat p (p * m + n)! = padicValNat p (p * m)!
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
p n m : ℕ
hp : Fact (Nat.Prime p)
h✝ : n < p
h : zero < p
⊢ padicValNat p (p * m + zero)! = padicValNat p (p * m)!
[PROOFSTEP]
rw [zero_eq, add_zero]
[GOAL]
case succ
p n✝ m : ℕ
hp : Fact (Nat.Prime p)
h✝ : n✝ < p
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : succ n < p
⊢ padicValNat p (p * m + succ n)! = padicValNat p (p * m)!
[PROOFSTEP]
rw [add_succ, factorial_succ, padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
  hn <| lt_of_succ_lt h, ← add_succ,
  padicValNat_eq_zero_of_mem_Ioo
    ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
      (Nat.mul_add _ _ _ ▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
  zero_add]
[GOAL]
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * (n / p))! = padicValNat p n !
[PROOFSTEP]
nth_rw 2 [← div_add_mod n p]
[GOAL]
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * (n / p))! = padicValNat p (p * (n / p) + n % p)!
[PROOFSTEP]
exact (padicValNat_factorial_mul_add (n / p) <| mod_lt n <| Prime.pos hp.out).symm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * padicValNat p n ! = n - List.sum (digits p n)
[PROOFSTEP]
rw [padicValNat_factorial <| lt_succ_of_lt <| lt.base (log p n), ← Finset.sum_Ico_add' _ 0 _ 1, Ico_zero_eq_range, ←
  sub_one_mul_sum_log_div_pow_eq_sub_sum_digits]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a
[PROOFSTEP]
rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff, ← Int.coe_nat_dvd_left, Int.coe_nat_pow]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ ↑p ^ padicValInt p a ∣ a
[PROOFSTEP]
rw [padicValInt_dvd_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ a = 0 ∨ padicValInt p a ≤ padicValInt p a
[PROOFSTEP]
exact Or.inr le_rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValInt p (a * b) = padicValInt p a + padicValInt p b
[PROOFSTEP]
simp_rw [padicValInt]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValNat p (Int.natAbs (a * b)) = padicValNat p (Int.natAbs a) + padicValNat p (Int.natAbs b)
[PROOFSTEP]
rw [Int.natAbs_mul, padicValNat.mul]
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ Int.natAbs a ≠ 0
[PROOFSTEP]
rwa [Int.natAbs_ne_zero]
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ Int.natAbs b ≠ 0
[PROOFSTEP]
rwa [Int.natAbs_ne_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p (a * ↑p) = padicValInt p a + 1
[PROOFSTEP]
rw [padicValInt.mul ha (Int.coe_nat_ne_zero.mpr hp.out.ne_zero)]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p a + padicValInt p ↑p = padicValInt p a + 1
[PROOFSTEP]
simp only [eq_self_iff_true, padicValInt.of_nat, padicValNat_self]