-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
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})
hdisj :
  Disjoint ({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})
x : ℕ × ℕ
this : x.2 * p ≤ x.1 * q ∨ x.1 * q ≤ x.2 * p
inl :
  ∀ (this : x.2 * p ≤ x.1 * q),
    ((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
inr :
  ∀ (this : 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
inl₁ :
  ∀ (this : x.2 * p ≤ x.1 * q),
    ((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
inr₁ :
  ∀ (this : 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
inl₂ :
  ∀ (this : x.2 * p ≤ x.1 * q),
    ((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
inl₃ :
  ∀ (this : x.2 * p ≤ x.1 * q),
    (1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ →
      ((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
inr₂ :
  ∀ (this : 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
inr₃ :
  ∀ (this : x.1 * q ≤ x.2 * p),
    (1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ →
      ((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
inl₄ :
  ∀ (this : x.2 * p ≤ x.1 * q),
    x.2 * p ≤ x.1 * q →
      1 ≤ x.1 →
        x.1 < (p / 2).succ →
          1 ≤ x.2 → x.2 < (q / 2).succ → (1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ
inl₅ :
  ∀ (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 → (1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ
inl₆ :
  ∀ (this : x.2 * p ≤ x.1 * q),
    x.2 * p ≤ x.1 * q →
      1 ≤ x.1 →
        x.1 < (p / 2).succ →
          1 ≤ x.2 → x.2 < (q / 2).succ → (1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ
inl₇ :
  ∀ (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 → (1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ
inl₈ :
  ∀ (this : x.2 * p ≤ x.1 * q),
    x.2 * p ≤ x.1 * q → 1 ≤ x.1 → x.1 < (p / 2).succ → 1 ≤ x.2 → x.2 < (q / 2).succ → 1 ≤ x.1
inl₉ :
  ∀ (this : x.2 * p ≤ x.1 * q),
    x.2 * p ≤ x.1 * q → 1 ≤ x.1 → x.1 < (p / 2).succ → 1 ≤ x.2 → x.2 < (q / 2).succ → x.1 < (p / 2).succ
inl₁₀ :
  ∀ (this : x.2 * p ≤ x.1 * q),
    x.2 * p ≤ x.1 * q → 1 ≤ x.1 → x.1 < (p / 2).succ → 1 ≤ x.2 → x.2 < (q / 2).succ → 1 ≤ x.2
inl₁₁ :
  ∀ (this : x.2 * p ≤ x.1 * q),
    x.2 * p ≤ x.1 * q → 1 ≤ x.1 → x.1 < (p / 2).succ → 1 ≤ x.2 → x.2 < (q / 2).succ → x.2 < (q / 2).succ
inl₁₂ :
  ∀ (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 → 1 ≤ x.1
inl₁₃ :
  ∀ (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.1 < (p / 2).succ
inl₁₄ :
  ∀ (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 → 1 ≤ x.2
inl₁₅ :
  ∀ (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 < (q / 2).succ
⊢ ((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
have inl₁₆ : ∀ (this : x.2 * p ≤ x.1 * q),
  1 ≤ x.1 →
    x.1 < (p / 2).succ →
      1 ≤ x.2 →
        x.2 < (q / 2).succ →
          ((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
Tactic: tauto
Cleared hypotheses: this