-- Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
theorem sum_mul_div_add_sum_mul_div_eq_mul (p q : ℕ) [hp : Fact p.Prime] (hq0 : (q : ZMod p) ≠ 0) :
    ∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q =
    p / 2 * (q / 2)

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
this : (↑x.1).val = val 0
⊢ False

Tactic:
rw [val_cast_of_lt hxp, val_zero] at this

Result:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
this : x.1 = 0
⊢ False

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
hdisj :
  Disjoint (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))
x : ℕ × ℕ
this : x.2 * p ≤ x.1 * q ∨ x.1 * q ≤ x.2 * p
⊢ x ∈
      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) ↔
    x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ

Tactic:
simp only [mem_union, mem_filter, mem_Ico, mem_product]

Result:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
hdisj :
  Disjoint (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))
x : ℕ × ℕ
this : x.2 * p ≤ x.1 * q ∨ x.1 * q ≤ x.2 * p
⊢ ((1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ) ∧ x.2 * p ≤ x.1 * q ∨
      ((1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ) ∧ x.1 * q ≤ x.2 * p ↔
    (1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
⊢ x.1 ≤ p / 2

Tactic:
simp_all only [Nat.lt_succ_iff, mem_Ico, mem_product]

Result:
no goals

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
hdisj :
  Disjoint (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))
⊢ ∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)

Tactic:
have hunion :
    {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | 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

Result:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
hdisj :
  Disjoint (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))
hunion :
  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) =
    Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
⊢ ∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
⊢ ∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)

Tactic:
have hswap :
  #{x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p} =
    #{x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} :=
  card_equiv (Equiv.prodComm _ _)
    (fun ⟨_, _⟩ => by
      simp +contextual only [mem_filter, and_self_iff, Prod.swap_prod_mk,
        forall_true_iff, mem_product, Equiv.prodComm_apply, and_assoc, and_left_comm])

Result:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
⊢ ∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
this : x.1 = 0
⊢ False

Tactic:
simp only [this, nonpos_iff_eq_zero, mem_Ico, one_ne_zero, false_and, mem_product] at hx

Result:
no goals

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
hdisj :
  Disjoint (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))
hunion :
  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) =
    Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
⊢ ∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)

Tactic:
rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_union_of_disjoint hdisj, hunion,
  card_product]

Result:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
hdisj :
  Disjoint (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))
hunion :
  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) =
    Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
⊢ #(Ico 1 (p / 2).succ) * #(Ico 1 (q / 2).succ) = p / 2 * (q / 2)