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

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

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

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

State before:
case succ
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x < x * y + 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 < x * y

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

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

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

State before:
case succ.a.hb
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