Theorem: Pos.not_lt_one (Extra/Pos/Lemmas.lean)

State before:
x : Pos
⊢ ¬x < 1
Tactic:
by_toNat
State after:
x : Pos
⊢ ¬1 > x.toNat

State before:
x : Pos
⊢ ¬1 > x.toNat
Tactic:
intro h
State after:
x : Pos
h : 1 > x.toNat
⊢ False

State before:
x : Pos
h : 1 > x.toNat
⊢ False
Tactic:
absurd h
State after:
x : Pos
h : 1 > x.toNat
⊢ ¬1 > x.toNat

State before:
x : Pos
h : 1 > x.toNat
⊢ ¬1 > x.toNat
Tactic:
apply Nat.not_lt_of_ge
State after:
case a
x : Pos
h : 1 > x.toNat
⊢ x.toNat ≥ 1

State before:
case a
x : Pos
h : 1 > x.toNat
⊢ x.toNat ≥ 1
Tactic:
apply Nat.succ_le_of_lt
State after:
case a.h
x : Pos
h : 1 > x.toNat
⊢ 0 < x.toNat

State before:
case a.h
x : Pos
h : 1 > x.toNat
⊢ 0 < x.toNat
Tactic:
exact Nat.zero_lt _
State after:
no goals