-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem div_sat (c : Constraint) (t : Int) (k : Nat) (n : k ≠ 0) (h : (k : Int) ∣ t) (w : c.sat t) :
    (c.div k).sat (t / k)

Proof state:
case mk.none.some.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
u : Int
w : t ≤ u
⊢ 0 ≤ u / ↑k - t / ↑k

Tactic:
rw [← Int.sub_ediv_of_dvd _ h, ← ge_iff_le, Int.div_nonneg_iff_of_pos n]

Result:
case mk.none.some.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
u : Int
w : t ≤ u
⊢ u - t ≥ 0

Proof state:
case mk.none.none
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
w : { lowerBound := none, upperBound := none }.sat t = true
⊢ ({ lowerBound := none, upperBound := none }.div k).sat (t / ↑k) = true

Tactic:
simp_all [sat, div]

Result:
no goals

Proof state:
case mk.none.some
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
u : Int
w : { lowerBound := none, upperBound := some u }.sat t = true
⊢ ({ lowerBound := none, upperBound := some u }.div k).sat (t / ↑k) = true

Tactic:
simp [sat, div] at w ⊢

Result:
case mk.none.some
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
u : Int
w : t ≤ u
⊢ t / ↑k ≤ u / ↑k

Proof state:
case mk.some.some
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : { lowerBound := some l, upperBound := some u }.sat t = true
⊢ ({ lowerBound := some l, upperBound := some u }.div k).sat (t / ↑k) = true

Tactic:
simp [sat, div] at w ⊢

Result:
case mk.some.some
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ -(-l / ↑k) ≤ t / ↑k ∧ t / ↑k ≤ u / ↑k

Proof state:
case mk.some.none
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l : Int
w : { lowerBound := some l, upperBound := none }.sat t = true
⊢ ({ lowerBound := some l, upperBound := none }.div k).sat (t / ↑k) = true

Tactic:
simp [sat, div] at w ⊢

Result:
case mk.some.none
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l : Int
w : l ≤ t
⊢ -(-l / ↑k) ≤ t / ↑k

Proof state:
case mk.none.some.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
u : Int
w : t ≤ u
⊢ u - t ≥ 0

Tactic:
exact Int.sub_nonneg_of_le w

Result:
no goals

Proof state:
case mk.none.some
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
u : Int
w : t ≤ u
⊢ t / ↑k ≤ u / ↑k

Tactic:
apply Int.le_of_sub_nonneg

Result:
case mk.none.some.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
u : Int
w : t ≤ u
⊢ 0 ≤ u / ↑k - t / ↑k

Proof state:
case mk.some.some.right.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ u - t ≥ 0

Tactic:
exact Int.sub_nonneg_of_le w.2

Result:
no goals

Proof state:
case mk.some.some
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ -(-l / ↑k) ≤ t / ↑k ∧ t / ↑k ≤ u / ↑k

Tactic:
constructor

Result:
case mk.some.some.left
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ -(-l / ↑k) ≤ t / ↑k

case mk.some.some.right
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ t / ↑k ≤ u / ↑k

Proof state:
c : Constraint
t : Int
k : Nat
h : ↑k ∣ t
w : c.sat t = true
n : ↑k > 0
⊢ (c.div k).sat (t / ↑k) = true

Tactic:
rcases c with ⟨_ | l, _ | u⟩

Result:
case mk.none.none
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
w : { lowerBound := none, upperBound := none }.sat t = true
⊢ ({ lowerBound := none, upperBound := none }.div k).sat (t / ↑k) = true

case mk.none.some
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
u : Int
w : { lowerBound := none, upperBound := some u }.sat t = true
⊢ ({ lowerBound := none, upperBound := some u }.div k).sat (t / ↑k) = true

case mk.some.none
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l : Int
w : { lowerBound := some l, upperBound := none }.sat t = true
⊢ ({ lowerBound := some l, upperBound := none }.div k).sat (t / ↑k) = true

case mk.some.some
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : { lowerBound := some l, upperBound := some u }.sat t = true
⊢ ({ lowerBound := some l, upperBound := some u }.div k).sat (t / ↑k) = true

Proof state:
case mk.some.some.right.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ 0 ≤ u / ↑k - t / ↑k

Tactic:
rw [← Int.sub_ediv_of_dvd _ h, ← ge_iff_le, Int.div_nonneg_iff_of_pos n]

Result:
case mk.some.some.right.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ u - t ≥ 0

Proof state:
case mk.some.none.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l : Int
w : l ≤ t
⊢ t + -l ≥ 0

Tactic:
exact Int.sub_nonneg_of_le w

Result:
no goals

Proof state:
case mk.some.none
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l : Int
w : l ≤ t
⊢ -(-l / ↑k) ≤ t / ↑k

Tactic:
apply Int.le_of_sub_nonneg

Result:
case mk.some.none.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l : Int
w : l ≤ t
⊢ 0 ≤ t / ↑k - -(-l / ↑k)

Proof state:
case mk.some.some.left
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ -(-l / ↑k) ≤ t / ↑k

Tactic:
apply Int.le_of_sub_nonneg

Result:
case mk.some.some.left.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ 0 ≤ t / ↑k - -(-l / ↑k)

Proof state:
c : Constraint
t : Int
k : Nat
n : k ≠ 0
h : ↑k ∣ t
w : c.sat t = true
⊢ (c.div k).sat (t / ↑k) = true

Tactic:
replace n : (k : Int) > 0 := Int.ofNat_lt.mpr (Nat.pos_of_ne_zero n)

Result:
c : Constraint
t : Int
k : Nat
h : ↑k ∣ t
w : c.sat t = true
n : ↑k > 0
⊢ (c.div k).sat (t / ↑k) = true

Proof state:
case mk.some.none.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l : Int
w : l ≤ t
⊢ 0 ≤ t / ↑k - -(-l / ↑k)

Tactic:
rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, ← ge_iff_le,
  Int.div_nonneg_iff_of_pos n]

Result:
case mk.some.none.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l : Int
w : l ≤ t
⊢ t + -l ≥ 0

Proof state:
case mk.some.some.left.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ 0 ≤ t / ↑k - -(-l / ↑k)

Tactic:
rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, ← ge_iff_le,
  Int.div_nonneg_iff_of_pos n]

Result:
case mk.some.some.left.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ t + -l ≥ 0

Proof state:
case mk.some.some.right
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ t / ↑k ≤ u / ↑k

Tactic:
apply Int.le_of_sub_nonneg

Result:
case mk.some.some.right.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ 0 ≤ u / ↑k - t / ↑k

Proof state:
case mk.some.some.left.h
t : Int
k : Nat
h : ↑k ∣ t
n : ↑k > 0
l u : Int
w : l ≤ t ∧ t ≤ u
⊢ t + -l ≥ 0

Tactic:
exact Int.sub_nonneg_of_le w.1

Result:
no goals