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

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

Tactic:
simp only [gcd_neg, Int.neg_mul_neg] at h

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

Proof state:
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
⊢ ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro.intro.refine_3
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
h :
  ∃ k,
    0 ≤ k ∧
      k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
        a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s
x : Int
lower : -q ≤ b * x
upper : a * x ≤ -p
dvd : d ∣ -c * x + s
⊢ d ∣ c * -x + s

Tactic:
exact Int.mul_neg _ _ ▸ Int.neg_mul _ _ ▸ dvd

Result:
no goals

Proof state:
case mp
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s) →
    ∃ k,
      0 ≤ k ∧
        k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
          a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s

Tactic:
rintro ⟨x, lower, upper, dvd⟩

Result:
case mp.intro.intro.intro
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
x : Int
lower : p ≤ a * x
upper : b * x ≤ q
dvd : d ∣ c * x + s
⊢ ∃ k,
    0 ≤ k ∧
      k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
        a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s

Proof state:
case mpr
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
⊢ (∃ k,
      0 ≤ k ∧
        k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
          a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s) →
    ∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s

Tactic:
intro h

Result:
case mpr
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
h :
  ∃ k,
    0 ≤ k ∧
      k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
        a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s
⊢ ∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s

Proof state:
case mp.intro.intro.intro
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
x : Int
lower : p ≤ a * x
upper : b * x ≤ q
dvd : d ∣ c * x + s
⊢ ∃ k,
    0 ≤ k ∧
      k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
        a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s

Tactic:
have h : (∃ x, -q ≤ b * x ∧ a * x ≤ -p ∧ d ∣ -c * x + s) :=
  ⟨-x, Int.mul_neg _ _ ▸ Int.neg_le_neg upper, Int.mul_neg _ _ ▸ Int.neg_le_neg lower,
    by rwa [Int.neg_mul_neg _ _]⟩

Result:
case mp.intro.intro.intro
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
x : Int
lower : p ≤ a * x
upper : b * x ≤ q
dvd : d ∣ c * x + s
h : ∃ x, -q ≤ b * x ∧ a * x ≤ -p ∧ d ∣ -c * x + s
⊢ ∃ k,
    0 ≤ k ∧
      k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
        a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s

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

Tactic:
exact h

Result:
no goals

Proof state:
case mpr.intro.intro.intro
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
h :
  ∃ k,
    0 ≤ k ∧
      k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
        a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s
x : Int
lower : -q ≤ b * x
upper : a * x ≤ -p
dvd : d ∣ -c * x + s
⊢ ∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s

Tactic:
refine ⟨-x, ?_, ?_, ?_⟩

Result:
case mpr.intro.intro.intro.refine_1
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
h :
  ∃ k,
    0 ≤ k ∧
      k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
        a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s
x : Int
lower : -q ≤ b * x
upper : a * x ≤ -p
dvd : d ∣ -c * x + s
⊢ p ≤ a * -x

case mpr.intro.intro.intro.refine_2
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
h :
  ∃ k,
    0 ≤ k ∧
      k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
        a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s
x : Int
lower : -q ≤ b * x
upper : a * x ≤ -p
dvd : d ∣ -c * x + s
⊢ b * -x ≤ q

case mpr.intro.intro.intro.refine_3
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
h :
  ∃ k,
    0 ≤ k ∧
      k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
        a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s
x : Int
lower : -q ≤ b * x
upper : a * x ≤ -p
dvd : d ∣ -c * x + s
⊢ d ∣ c * -x + s

Proof state:
case mpr
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
h :
  ∃ k,
    0 ≤ k ∧
      k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
        a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s
⊢ ∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s

Tactic:
obtain ⟨x, lower, upper, dvd⟩ := (cooper_resolution_dvd_left b_pos a_pos d_pos).mpr h

Result:
case mpr.intro.intro.intro
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
this : ∀ (x y z : Int), x + -y ≤ -z ↔ x + z ≤ y
h :
  ∃ k,
    0 ≤ k ∧
      k < ↑(b.lcm (b * d / ↑((b * d).gcd (-c)))) ∧
        a * k + a * -q ≤ b * -p ∧ b ∣ k + -q ∧ b * d ∣ -c * k + -c * -q + b * s
x : Int
lower : -q ≤ b * x
upper : a * x ≤ -p
dvd : d ∣ -c * x + s
⊢ ∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s