Theorem: Nat.lt_mul_of_gt_one_of_pos_left (GMLInit/Data/Nat/Mul.lean)

State before:
x y : Nat
h : autoParam (x > 0) _auto✝
⊢ y > 1 → x < y * x
Tactic:
intro hy
State after:
x y : Nat
h : autoParam (x > 0) _auto✝
hy : y > 1
⊢ x < y * x

State before:
case zero
x : Nat
h : autoParam (x > 0) _auto✝
hy : 0 > 1
⊢ x < 0 * x
Tactic:
contradiction
State after:
no goals

State before:
case succ
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x < (y + 1) * x
Tactic:
rw [Nat.succ_mul]
State after:
case succ
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x < y * x + x

State before:
case succ
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x < y * x + x
Tactic:
apply Nat.lt_add_of_pos_left
State after:
case succ.a
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ 0 < y * x

State before:
case succ.a
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ 0 < y * x
Tactic:
apply Nat.mul_pos
State after:
case succ.a.ha
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ y > 0

case succ.a.hb
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x > 0

State before:
case succ.a.ha
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ y > 0
Tactic:
exact Nat.lt_of_succ_lt_succ hy
State after:
no goals

State before:
case succ.a.hb
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x > 0
Tactic:
exact h
State after:
no goals