-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem cooper_resolution_dvd_left
    {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 a (a * d / gcd (a * d) c) ∧
      b * k + b * p ≤ a * q ∧
      a ∣ k + p ∧
      a * d ∣ c * k + c * p + a * 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
⊢ (∃ k,
      0 ≤ k ∧
        k < ↑(a.lcm (a * d / ↑((a * d).gcd c))) ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p ∧ a * d ∣ c * k + c * p + a * s) →
    ∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s

Tactic:
rintro ⟨k, h₁, h₂, h₃, h₄, h₅⟩

Result:
case mpr.intro.intro.intro.intro.intro
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
k : Int
h₁ : 0 ≤ k
h₂ : k < ↑(a.lcm (a * d / ↑((a * d).gcd c)))
h₃ : b * k + b * p ≤ a * q
h₄ : a ∣ k + p
h₅ : a * d ∣ c * k + c * p + a * 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
x : Int
h₁ : p ≤ a * x
h₂ : b * x ≤ q
h₃ : d ∣ c * x + s
⊢ ∃ k,
    0 ≤ k ∧ k < ↑(a.lcm (a * d / ↑((a * d).gcd c))) ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p ∧ a * d ∣ c * k + c * p + a * s

Tactic:
exact ⟨resolve_left a c d p x,
  le_zero_resolve_left a c d p x h₁,
  resolve_left_lt_lcm a c d p x a_pos d_pos h₁,
  resolve_left_ineq a c d p x a_pos b_pos h₁ h₂,
  resolve_left_dvd₁ a c d p x h₁,
  resolve_left_dvd₂ a c d p x h₁ h₃⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro
a b c d s p q : Int
a_pos : 0 < a
b_pos : 0 < b
d_pos : 0 < d
k : Int
h₁ : 0 ≤ k
h₂ : k < ↑(a.lcm (a * d / ↑((a * d).gcd c)))
h₃ : b * k + b * p ≤ a * q
h₄ : a ∣ k + p
h₅ : a * d ∣ c * k + c * p + a * s
⊢ ∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s

Tactic:
exact ⟨resolve_left_inv a p k,
  le_mul_resolve_left_inv a p k h₁ h₄,
  mul_resolve_left_inv_le a p k a_pos h₃ h₄,
  resolve_left_inv_dvd a c d p k a_pos h₄ h₅⟩

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
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s) →
    ∃ k,
      0 ≤ k ∧
        k < ↑(a.lcm (a * d / ↑((a * d).gcd c))) ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p ∧ a * d ∣ c * k + c * p + a * s

Tactic:
rintro ⟨x, h₁, h₂, 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
x : Int
h₁ : p ≤ a * x
h₂ : b * x ≤ q
h₃ : d ∣ c * x + s
⊢ ∃ k,
    0 ≤ k ∧ k < ↑(a.lcm (a * d / ↑((a * d).gcd c))) ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p ∧ a * d ∣ c * k + c * p + a * s

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 < ↑(a.lcm (a * d / ↑((a * d).gcd c))) ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p ∧ a * d ∣ c * k + c * p + a * 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
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s) →
    ∃ k,
      0 ≤ k ∧
        k < ↑(a.lcm (a * d / ↑((a * d).gcd c))) ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p ∧ a * d ∣ c * k + c * p + a * s

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