-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem cooper_resolution_right
    {a b p q : Int} (a_pos : 0 < a) (b_pos : 0 < b) :
    (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔
    (∃ k : Int, 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q)

Proof state:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
h :
  (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ 1 ∣ 1 * x + 0) ↔
    ∃ k,
      0 ≤ k ∧
        k < ↑(b.lcm (b * 1 / ↑((b * 1).gcd 1))) ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q ∧ b * 1 ∣ -1 * k + 1 * q + b * 0
this : ∀ (k : Int), b ∣ -k + q ↔ b ∣ k - q
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q

Tactic:
simp only [Int.mul_one, Int.one_mul, Int.mul_zero, Int.add_zero, gcd_one, Int.ofNat_one,
  Int.ediv_one, lcm_self, Int.natAbs_of_nonneg (Int.le_of_lt b_pos), Int.one_dvd, and_true,
  and_self, ← Int.neg_eq_neg_one_mul, this] at h

Result:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
this : ∀ (k : Int), b ∣ -k + q ↔ b ∣ k - q
h : (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q

Proof state:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
h :
  (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ 1 ∣ 1 * x + 0) ↔
    ∃ k,
      0 ≤ k ∧
        k < ↑(b.lcm (b * 1 / ↑((b * 1).gcd 1))) ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q ∧ b * 1 ∣ -1 * k + 1 * q + b * 0
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q

Tactic:
have : ∀ k : Int, (b ∣ -k + q) ↔ (b ∣ k - q) := by
  intro k
  rw [← Int.dvd_neg, Int.neg_add, Int.neg_neg, Int.sub_eq_add_neg]

Result:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
h :
  (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ 1 ∣ 1 * x + 0) ↔
    ∃ k,
      0 ≤ k ∧
        k < ↑(b.lcm (b * 1 / ↑((b * 1).gcd 1))) ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q ∧ b * 1 ∣ -1 * k + 1 * q + b * 0
this : ∀ (k : Int), b ∣ -k + q ↔ b ∣ k - q
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q

Proof state:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
h :
  (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ 1 ∣ 1 * x + 0) ↔
    ∃ k,
      0 ≤ k ∧
        k < ↑(b.lcm (b * 1 / ↑((b * 1).gcd 1))) ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q ∧ b * 1 ∣ -1 * k + 1 * q + b * 0
k : Int
⊢ b ∣ -k + q ↔ b ∣ k - q

Tactic:
rw [← Int.dvd_neg, Int.neg_add, Int.neg_neg, Int.sub_eq_add_neg]

Result:
no goals

Proof state:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
this : ∀ (k : Int), b ∣ -k + q ↔ b ∣ k - q
h : (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q

Tactic:
exact h

Result:
no goals

Proof state:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q

Tactic:
have h := cooper_resolution_dvd_right
  a_pos b_pos Int.zero_lt_one (c := 1) (s := 0) (p := p) (q := q)

Result:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
h :
  (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ 1 ∣ 1 * x + 0) ↔
    ∃ k,
      0 ≤ k ∧
        k < ↑(b.lcm (b * 1 / ↑((b * 1).gcd 1))) ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q ∧ b * 1 ∣ -1 * k + 1 * q + b * 0
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q

Proof state:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
h :
  (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ 1 ∣ 1 * x + 0) ↔
    ∃ k,
      0 ≤ k ∧
        k < ↑(b.lcm (b * 1 / ↑((b * 1).gcd 1))) ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q ∧ b * 1 ∣ -1 * k + 1 * q + b * 0
⊢ ∀ (k : Int), b ∣ -k + q ↔ b ∣ k - q

Tactic:
intro k

Result:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
h :
  (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ 1 ∣ 1 * x + 0) ↔
    ∃ k,
      0 ≤ k ∧
        k < ↑(b.lcm (b * 1 / ↑((b * 1).gcd 1))) ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q ∧ b * 1 ∣ -1 * k + 1 * q + b * 0
k : Int
⊢ b ∣ -k + q ↔ b ∣ k - q