Theorem: Nat.le_of_mul_le_mul_of_pos_left (Extra/Nat/Lemmas.lean)

State before:
x y z : Nat
⊢ 0 < x → x * y ≤ x * z → y ≤ z
Tactic:
intro hx hxyz
State after:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
⊢ y ≤ z

State before:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
⊢ y ≤ z
Tactic:
if h : z < y then
  absurd hxyz
  apply Nat.not_le_of_gt
  exact Nat.mul_lt_mul_of_pos_left h hx
else
  exact Nat.le_of_not_gt h
State after:
no goals

State before:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : z < y
⊢ y ≤ z
Tactic:
absurd hxyz
State after:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : z < y
⊢ ¬x * y ≤ x * z

State before:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : z < y
⊢ ¬x * y ≤ x * z
Tactic:
apply Nat.not_le_of_gt
State after:
case h
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : z < y
⊢ x * y > x * z

State before:
case h
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : z < y
⊢ x * y > x * z
Tactic:
exact Nat.mul_lt_mul_of_pos_left h hx
State after:
no goals

State before:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : ¬z < y
⊢ y ≤ z
Tactic:
exact Nat.le_of_not_gt h
State after:
no goals