-- Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
theorem gauss_lemma_aux₁ (p : ℕ) [Fact p.Prime] {a : ℤ} (hap : (a : ZMod p) ≠ 0) :
    (a ^ (p / 2) * (p / 2)! : ZMod p) =
     (-1 : ZMod p) ^ #{x ∈ Ico 1 (p / 2).succ | ¬ (a * x.cast : ZMod p).val ≤ p / 2} * (p / 2)! :=
  calc
    (a ^ (p / 2) * (p / 2)! : ZMod p) = ∏ x ∈ Ico 1 (p / 2).succ, a * x

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑(∏ x ∈ Ico 1 (p / 2).succ, a * ↑x)

Tactic:
rw [prod_mul_distrib, ← prod_natCast, prod_Ico_id_eq_factorial, prod_const, card_Ico,
  Nat.add_one_sub_one]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑(a ^ (p / 2) * ↑(p / 2)!)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ∀ a_1 ∈ Ico 1 (p / 2).succ,
    (if (↑a * ↑a_1).val ≤ p / 2 then 1 else -1) ≠ 1 → (if (↑a * ↑a_1).val ≤ p / 2 then 1 else -1) = -1

Tactic:
intros

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
a✝ : ℕ
h₁✝ : a✝ ∈ Ico 1 (p / 2).succ
h₂✝ : (if (↑a * ↑a✝).val ≤ p / 2 then 1 else -1) ≠ 1
⊢ (if (↑a * ↑a✝).val ≤ p / 2 then 1 else -1) = -1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑(a ^ (p / 2) * ↑(p / 2)!)

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑(∏ x ∈ Ico 1 (p / 2).succ, a * ↑x) = ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).val

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x : ℕ
⊢ ∀ (h₁ : x ∈ Ico 1 (p / 2).succ) (h₂ : (if (↑a * ↑x).val ≤ p / 2 then 1 else -1) ≠ 1),
    (fun x x_1 x_2 => x) x h₁ h₂ ∈ filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)

Tactic:
split_ifs <;> (dsimp; simp_all)

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (p / 2).succ
⊢ ↑(↑a * ↑x✝¹).val =
    (if (↑a * ↑x✝¹).val ≤ p / 2 then 1 else -1) * if (↑a * ↑x✝¹).val ≤ p / 2 then ↑a * ↑x✝¹ else -(↑a * ↑x✝¹)

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
b : ℕ
h : b ∈ filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)
x✝ : -1 ≠ 1
⊢ ∃ (h₁ : b ∈ Ico 1 (p / 2).succ) (h₂ : (if (↑a * ↑b).val ≤ p / 2 then 1 else -1) ≠ 1), (fun x x_1 x_2 => x) b h₁ h₂ = b

Tactic:
simp_all [-not_le]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ∏ x ∈ Ico 1 (p / 2).succ, (if (↑a * ↑x).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #(filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)) *
      ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs

Tactic:
have :
    (∏ x ∈ Ico 1 (p / 2).succ, if (a * x : ZMod p).val ≤ p / 2 then (1 : ZMod p) else -1) =
    ∏ x ∈ Ico 1 (p / 2).succ with ¬(a * x.cast : ZMod p).val ≤ p / 2, -1 :=
  prod_bij_ne_one (fun x _ _ => x)
    (fun x => by split_ifs <;> (dsimp; simp_all))
    (fun _ _ _ _ _ _ => id) (fun b h _ => ⟨b, by simp_all [-not_le]⟩)
    (by intros; split_ifs at * <;> simp_all)

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
this :
  (∏ x ∈ Ico 1 (p / 2).succ, if (↑a * ↑x).val ≤ p / 2 then 1 else -1) =
    ∏ x ∈ filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ), -1
⊢ ∏ x ∈ Ico 1 (p / 2).succ, (if (↑a * ↑x).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #(filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)) *
      ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
a✝ : ℕ
h₁✝ : a✝ ∈ Ico 1 (p / 2).succ
h₂✝ : (if (↑a * ↑a✝).val ≤ p / 2 then 1 else -1) ≠ 1
⊢ (if (↑a * ↑a✝).val ≤ p / 2 then 1 else -1) = -1

Tactic:
split_ifs at * <;> simp_all

Result:
no goals

Proof state:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x : ℕ
h✝ : ¬(↑a * ↑x).val ≤ p / 2
⊢ ∀ (h₁ : x ∈ Ico 1 (p / 2).succ) (h₂ : -1 ≠ 1),
    (fun x x_1 x_2 => x) x h₁ ⋯ ∈ filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)

Tactic:
dsimp

Result:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x : ℕ
h✝ : ¬(↑a * ↑x).val ≤ p / 2
⊢ x ∈ Ico 1 (p / 2 + 1) → ¬-1 = 1 → x ∈ filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2 + 1))

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
this :
  (∏ x ∈ Ico 1 (p / 2).succ, if (↑a * ↑x).val ≤ p / 2 then 1 else -1) =
    ∏ x ∈ filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ), -1
⊢ ∏ x ∈ Ico 1 (p / 2).succ, (if (↑a * ↑x).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #(filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)) *
      ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs

Tactic:
rw [prod_mul_distrib, this, prod_const]

Result:
no goals

Proof state:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x : ℕ
h✝ : ¬(↑a * ↑x).val ≤ p / 2
⊢ x ∈ Ico 1 (p / 2 + 1) → ¬-1 = 1 → x ∈ filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2 + 1))

Tactic:
simp_all

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (p / 2).succ
⊢ ↑(↑a * ↑x✝¹).val = (if (↑a * ↑x✝¹).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x✝¹).valMinAbs.natAbs

Tactic:
simp only [natCast_natAbs_valMinAbs]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (p / 2).succ
⊢ ↑(↑a * ↑x✝¹).val =
    (if (↑a * ↑x✝¹).val ≤ p / 2 then 1 else -1) * if (↑a * ↑x✝¹).val ≤ p / 2 then ↑a * ↑x✝¹ else -(↑a * ↑x✝¹)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ (-1) ^ #(filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)) *
      ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #(filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Ico 1 (p / 2).succ)) * ↑(p / 2)!

Tactic:
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]

Result:
no goals