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

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

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

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

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

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

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