-- Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
theorem eisenstein_lemma_aux₁ (p : ℕ) [Fact p.Prime] [hp2 : Fact (p % 2 = 1)] {a : ℕ}
    (hap : (a : ZMod p) ≠ 0) :
    ((∑ x ∈ Ico 1 (p / 2).succ, a * x : ℕ) : ZMod 2) =
      #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val} +
        ∑ x ∈ Ico 1 (p / 2).succ, x + (∑ x ∈ Ico 1 (p / 2).succ, a * x / p : ℕ) :=
  have hp2 : (p : ZMod 2) = (1 : ℕ) := (eq_iff_modEq_nat _).2 hp2.1
  calc
    ((∑ x ∈ Ico 1 (p / 2).succ, a * x : ℕ) : ZMod 2) =
        ((∑ x ∈ Ico 1 (p / 2).succ, (a * x % p + p * (a * x / p)) : ℕ) : ZMod 2)

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

Tactic:
simp [add_comm, sum_add_distrib, Finset.sum_ite, hp2, Nat.cast_sum]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(#(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ))) +
      ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑a * ↑x).valMinAbs.natAbs) =
    ↑(#(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ))) + ↑(∑ x ∈ Ico 1 (p / 2).succ, x)

Tactic:
rw [Finset.sum_eq_multiset_sum, Ico_map_valMinAbs_natAbs_eq_Ico_map_id p a hap, ←
  Finset.sum_eq_multiset_sum]

Result:
no goals

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

Tactic:
simp only [mod_add_div]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑(a * x)).val) =
    ∑ x ∈ Ico 1 (p / 2).succ, ↑((↑a * ↑x).valMinAbs + ↑(if (↑a * ↑x).val ≤ p / 2 then 0 else p))

Tactic:
simp only [(val_eq_ite_valMinAbs _).symm]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑(a * x)).val) = ∑ x ∈ Ico 1 (p / 2).succ, ↑↑(↑a * ↑x).val

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

Tactic:
simp only [val_natCast]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x ∈ Ico 1 (p / 2).succ, (a * x % p + p * (a * x / p))) =
    ↑(∑ x ∈ Ico 1 (p / 2).succ, a * x % p) + ↑(∑ x ∈ Ico 1 (p / 2).succ, a * x / p)

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

Tactic:
simp [Nat.cast_sum]

Result:
no goals

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

Tactic:
simp [sum_add_distrib, ← mul_sum, Nat.cast_add, Nat.cast_mul, Nat.cast_sum, hp2]

Result:
no goals