Theorem: Int.mul_le_mul_left (Smt/Reconstruct/Int/Lemmas.lean)

State before:
c x y : Int
hc : c > 0
⊢ (c * x ≤ c * y) = (x ≤ y)
Tactic:
apply propext
State after:
case a
c x y : Int
hc : c > 0
⊢ c * x ≤ c * y ↔ x ≤ y

State before:
case a
c x y : Int
hc : c > 0
⊢ c * x ≤ c * y ↔ x ≤ y
Tactic:
constructor
State after:
case a.mp
c x y : Int
hc : c > 0
⊢ c * x ≤ c * y → x ≤ y

case a.mpr
c x y : Int
hc : c > 0
⊢ x ≤ y → c * x ≤ c * y

State before:
case a.mp
c x y : Int
hc : c > 0
⊢ c * x ≤ c * y → x ≤ y
Tactic:
apply le_of_mul_le_mul_left (h := hc)
State after:
no goals

State before:
case a.mpr
c x y : Int
hc : c > 0
⊢ x ≤ y → c * x ≤ c * y
Tactic:
apply Int.mul_le_mul_of_nonneg_left (h₂ := Int.le_of_lt hc)
State after:
no goals