-- 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:
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 :
  ∃ 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
⊢ ∃ 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:
exact h

Result:
no goals

Proof state:
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,
      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:
have this : ∀ x y z : Int, x + -y ≤ -z ↔ x + z ≤ y := by omega

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
⊢ (∃ 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
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 + b * p ≤ a * q ∧ b ∣ k - q ∧ b * d ∣ -c * k + c * q + b * s

Tactic:
suffices h :
  (∃ 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 + a * (-q) ≤ b * (-p) ∧
    b ∣ k + (-q) ∧
    b * d ∣ (- c) * k + (-c) * (-q) + b * s) by
  simp only [gcd_neg, Int.neg_mul_neg] at h
  simp only [Int.mul_neg, this] at h
  exact 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
⊢ (∃ 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

Proof state:
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

Tactic:
exact Int.mul_neg _ _ ▸ Int.le_neg_of_le_neg upper

Result:
no goals

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
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

Tactic:
replace h := (cooper_resolution_dvd_left b_pos a_pos d_pos).mp h

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 :
  ∃ 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
⊢ ∃ 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 + 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 [Int.mul_neg, this] 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 + 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

Proof state:
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

Tactic:
exact Int.mul_neg _ _ ▸ Int.neg_le_of_neg_le lower

Result:
no goals

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
⊢ (∃ 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:
constructor

Result:
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

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

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
x : Int
lower : p ≤ a * x
upper : b * x ≤ q
dvd : d ∣ c * x + s
⊢ d ∣ -c * -x + s

Tactic:
rwa [Int.neg_mul_neg _ _]

Result:
no goals