-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem scale_sat {c : Constraint} (k) (w : c.sat t) : (scale k c).sat (k * t)

Proof state:
case isFalse.mk.none.some.isFalse
t k : Int
h✝ : ¬k = 0
u : Int
w : t ≤ u
h : k ≤ 0
⊢ k * u ≤ k * t

Tactic:
exact Int.mul_le_mul_of_nonpos_left h w

Result:
no goals

Proof state:
case isTrue
t : Int
c : Constraint
k : Int
w : c.sat t = true
h✝ : k = 0
⊢ (if c.isImpossible = true then c else { lowerBound := some 0, upperBound := some 0 }).sat (k * t) = true

Tactic:
split

Result:
case isTrue.isTrue
t : Int
c : Constraint
k : Int
w : c.sat t = true
h✝¹ : k = 0
h✝ : c.isImpossible = true
⊢ c.sat (k * t) = true

case isTrue.isFalse
t : Int
c : Constraint
k : Int
w : c.sat t = true
h✝¹ : k = 0
h✝ : ¬c.isImpossible = true
⊢ { lowerBound := some 0, upperBound := some 0 }.sat (k * t) = true

Proof state:
t : Int
c : Constraint
k : Int
w : c.sat t = true
⊢ (if k = 0 then if c.isImpossible = true then c else { lowerBound := some 0, upperBound := some 0 }
        else if 0 < k then c.map fun x => k * x else c.flip.map fun x => k * x).sat
      (k * t) =
    true

Tactic:
split

Result:
case isTrue
t : Int
c : Constraint
k : Int
w : c.sat t = true
h✝ : k = 0
⊢ (if c.isImpossible = true then c else { lowerBound := some 0, upperBound := some 0 }).sat (k * t) = true

case isFalse
t : Int
c : Constraint
k : Int
w : c.sat t = true
h✝ : ¬k = 0
⊢ (if 0 < k then c.map fun x => k * x else c.flip.map fun x => k * x).sat (k * t) = true

Proof state:
case isFalse.mk.some.none.isTrue
t k : Int
h✝ : ¬k = 0
l : Int
w : l ≤ t
h : 0 < k
⊢ k * l ≤ k * t

Tactic:
replace h := Int.le_of_lt h

Result:
case isFalse.mk.some.none.isTrue
t k : Int
h✝ : ¬k = 0
l : Int
w : l ≤ t
h : 0 ≤ k
⊢ k * l ≤ k * t

Proof state:
case isFalse.mk.some.some.isFalse.left
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : k ≤ 0
⊢ k * u ≤ k * t

Tactic:
exact Int.mul_le_mul_of_nonpos_left h w.2

Result:
no goals

Proof state:
case isFalse.mk.none.some.isFalse
t k : Int
h✝ : ¬k = 0
u : Int
w : t ≤ u
h : ¬0 < k
⊢ k * u ≤ k * t

Tactic:
rw [Int.not_lt] at h

Result:
case isFalse.mk.none.some.isFalse
t k : Int
h✝ : ¬k = 0
u : Int
w : t ≤ u
h : k ≤ 0
⊢ k * u ≤ k * t

Proof state:
case isFalse.mk.none.some.isTrue
t k : Int
h✝ : ¬k = 0
u : Int
w : t ≤ u
h : 0 < k
⊢ k * t ≤ k * u

Tactic:
replace h := Int.le_of_lt h

Result:
case isFalse.mk.none.some.isTrue
t k : Int
h✝ : ¬k = 0
u : Int
w : t ≤ u
h : 0 ≤ k
⊢ k * t ≤ k * u

Proof state:
case isFalse
t : Int
c : Constraint
k : Int
w : c.sat t = true
h✝ : ¬k = 0
⊢ (if 0 < k then c.map fun x => k * x else c.flip.map fun x => k * x).sat (k * t) = true

Tactic:
rcases c with ⟨_ | l, _ | u⟩ <;> split <;> rename_i h <;> simp_all [sat, flip, map]

Result:
case isFalse.mk.none.some.isTrue
t k : Int
h✝ : ¬k = 0
u : Int
w : t ≤ u
h : 0 < k
⊢ k * t ≤ k * u

case isFalse.mk.none.some.isFalse
t k : Int
h✝ : ¬k = 0
u : Int
w : t ≤ u
h : ¬0 < k
⊢ k * u ≤ k * t

case isFalse.mk.some.none.isTrue
t k : Int
h✝ : ¬k = 0
l : Int
w : l ≤ t
h : 0 < k
⊢ k * l ≤ k * t

case isFalse.mk.some.none.isFalse
t k : Int
h✝ : ¬k = 0
l : Int
w : l ≤ t
h : ¬0 < k
⊢ k * t ≤ k * l

case isFalse.mk.some.some.isTrue
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : 0 < k
⊢ k * l ≤ k * t ∧ k * t ≤ k * u

case isFalse.mk.some.some.isFalse
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : ¬0 < k
⊢ k * u ≤ k * t ∧ k * t ≤ k * l

Proof state:
case isFalse.mk.some.some.isFalse
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : k ≤ 0
⊢ k * u ≤ k * t ∧ k * t ≤ k * l

Tactic:
constructor

Result:
case isFalse.mk.some.some.isFalse.left
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : k ≤ 0
⊢ k * u ≤ k * t

case isFalse.mk.some.some.isFalse.right
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : k ≤ 0
⊢ k * t ≤ k * l

Proof state:
case isFalse.mk.some.some.isTrue
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : 0 < k
⊢ k * l ≤ k * t ∧ k * t ≤ k * u

Tactic:
constructor

Result:
case isFalse.mk.some.some.isTrue.left
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : 0 < k
⊢ k * l ≤ k * t

case isFalse.mk.some.some.isTrue.right
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : 0 < k
⊢ k * t ≤ k * u

Proof state:
case isFalse.mk.some.none.isFalse
t k : Int
h✝ : ¬k = 0
l : Int
w : l ≤ t
h : ¬0 < k
⊢ k * t ≤ k * l

Tactic:
rw [Int.not_lt] at h

Result:
case isFalse.mk.some.none.isFalse
t k : Int
h✝ : ¬k = 0
l : Int
w : l ≤ t
h : k ≤ 0
⊢ k * t ≤ k * l

Proof state:
case isFalse.mk.some.some.isTrue.left
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : 0 < k
⊢ k * l ≤ k * t

Tactic:
exact Int.mul_le_mul_of_nonneg_left w.1 (Int.le_of_lt h)

Result:
no goals

Proof state:
case isFalse.mk.none.some.isTrue
t k : Int
h✝ : ¬k = 0
u : Int
w : t ≤ u
h : 0 ≤ k
⊢ k * t ≤ k * u

Tactic:
exact Int.mul_le_mul_of_nonneg_left w h

Result:
no goals

Proof state:
case isTrue.isTrue
t : Int
c : Constraint
k : Int
w : c.sat t = true
h✝¹ : k = 0
h✝ : c.isImpossible = true
⊢ c.sat (k * t) = true

Tactic:
simp_all [not_sat_of_isImpossible]

Result:
no goals

Proof state:
case isFalse.mk.some.some.isFalse
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : ¬0 < k
⊢ k * u ≤ k * t ∧ k * t ≤ k * l

Tactic:
replace h := Int.not_lt.mp h

Result:
case isFalse.mk.some.some.isFalse
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : k ≤ 0
⊢ k * u ≤ k * t ∧ k * t ≤ k * l

Proof state:
case isFalse.mk.some.none.isTrue
t k : Int
h✝ : ¬k = 0
l : Int
w : l ≤ t
h : 0 ≤ k
⊢ k * l ≤ k * t

Tactic:
exact Int.mul_le_mul_of_nonneg_left w h

Result:
no goals

Proof state:
case isFalse.mk.some.some.isFalse.right
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : k ≤ 0
⊢ k * t ≤ k * l

Tactic:
exact Int.mul_le_mul_of_nonpos_left h w.1

Result:
no goals

Proof state:
case isTrue.isFalse
t : Int
c : Constraint
k : Int
w : c.sat t = true
h✝¹ : k = 0
h✝ : ¬c.isImpossible = true
⊢ { lowerBound := some 0, upperBound := some 0 }.sat (k * t) = true

Tactic:
simp_all [sat]

Result:
no goals

Proof state:
case isFalse.mk.some.none.isFalse
t k : Int
h✝ : ¬k = 0
l : Int
w : l ≤ t
h : k ≤ 0
⊢ k * t ≤ k * l

Tactic:
exact Int.mul_le_mul_of_nonpos_left h w

Result:
no goals

Proof state:
t : Int
c : Constraint
k : Int
w : c.sat t = true
⊢ (scale k c).sat (k * t) = true

Tactic:
simp [scale]

Result:
t : Int
c : Constraint
k : Int
w : c.sat t = true
⊢ (if k = 0 then if c.isImpossible = true then c else { lowerBound := some 0, upperBound := some 0 }
        else if 0 < k then c.map fun x => k * x else c.flip.map fun x => k * x).sat
      (k * t) =
    true

Proof state:
case isFalse.mk.some.some.isTrue.right
t k : Int
h✝ : ¬k = 0
l u : Int
w : l ≤ t ∧ t ≤ u
h : 0 < k
⊢ k * t ≤ k * u

Tactic:
exact Int.mul_le_mul_of_nonneg_left w.2 (Int.le_of_lt h)

Result:
no goals