Theorem: Misc.Nat.mul_lt_mul_left (LeanSAT/Util/Misc.lean)

State before:
a b c : Nat
h : 0 < a
⊢ a * b < a * c ↔ b < c
Tactic:
constructor
State after:
case mp
a b c : Nat
h : 0 < a
⊢ a * b < a * c → b < c

case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c

State before:
case mp
a b c : Nat
h : 0 < a
⊢ a * b < a * c → b < c

case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c
Tactic:
. intro h
  exact Nat.gt_of_not_le fun hle : c ≤ b =>
    have : a * c ≤ a * b := Nat.mul_le_mul_left a hle
    have : ¬ a * b < a * c := Nat.not_lt_of_le this
    absurd h this
State after:
case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c

State before:
case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c
Tactic:
. intro h; apply Nat.mul_lt_mul_of_pos_left <;> assumption
State after:
no goals

State before:
case mp
a b c : Nat
h : 0 < a
⊢ a * b < a * c → b < c
Tactic:
intro h
State after:
case mp
a b c : Nat
h✝ : 0 < a
h : a * b < a * c
⊢ b < c

State before:
case mp
a b c : Nat
h✝ : 0 < a
h : a * b < a * c
⊢ b < c
Tactic:
exact Nat.gt_of_not_le fun hle : c ≤ b =>
  have : a * c ≤ a * b := Nat.mul_le_mul_left a hle
  have : ¬ a * b < a * c := Nat.not_lt_of_le this
  absurd h this
State after:
no goals

State before:
case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c
Tactic:
intro h
State after:
case mpr
a b c : Nat
h✝ : 0 < a
h : b < c
⊢ a * b < a * c

State before:
case mpr
a b c : Nat
h✝ : 0 < a
h : b < c
⊢ a * b < a * c
Tactic:
apply Nat.mul_lt_mul_of_pos_left <;> assumption
State after:
no goals