Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ (GMLInit/Data/Nat/Succ.lean)

State before:
case zero_left
x : Nat
⊢ 0 - 1 < x ∨ 0 = 0 ↔ 0 < x + 1
Tactic:
simp [Nat.zero_lt_succ]
State after:
no goals

State before:
case zero_right
y : Nat
⊢ y - 1 < 0 ∨ y = 0 ↔ y < 0 + 1
Tactic:
constructor
State after:
case zero_right.mp
y : Nat
⊢ y - 1 < 0 ∨ y = 0 → y < 0 + 1

case zero_right.mpr
y : Nat
⊢ y < 0 + 1 → y - 1 < 0 ∨ y = 0

State before:
case zero_right.mp
y : Nat
⊢ y - 1 < 0 ∨ y = 0 → y < 0 + 1
Tactic:
simp [Nat.not_lt_zero]
State after:
case zero_right.mp
y : Nat
⊢ y = 0 → y < 1

State before:
case zero_right.mp
y : Nat
⊢ y = 0 → y < 1
Tactic:
intro h
State after:
case zero_right.mp
y : Nat
h : y = 0
⊢ y < 1

State before:
case zero_right.mp
y : Nat
h : y = 0
⊢ y < 1
Tactic:
rw [h]
State after:
case zero_right.mp
y : Nat
h : y = 0
⊢ 0 < 1

State before:
case zero_right.mp
y : Nat
h : y = 0
⊢ 0 < 1
Tactic:
exact Nat.zero_lt_one
State after:
no goals

State before:
case zero_right.mpr
y : Nat
⊢ y < 0 + 1 → y - 1 < 0 ∨ y = 0
Tactic:
simp [Nat.not_lt_zero]
State after:
case zero_right.mpr
y : Nat
⊢ y < 1 → y = 0

State before:
case zero_right.mpr
y : Nat
⊢ y < 1 → y = 0
Tactic:
intro h
State after:
case zero_right.mpr
y : Nat
h : y < 1
⊢ y = 0

State before:
case zero_right.mpr
y : Nat
h : y < 1
⊢ y = 0
Tactic:
exact Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ h)
State after:
no goals

State before:
case succ_succ
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
⊢ x + 1 - 1 < y + 1 ∨ x + 1 = 0 ↔ x + 1 < y + 1 + 1
Tactic:
constructor
State after:
case succ_succ.mp
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
⊢ x + 1 - 1 < y + 1 ∨ x + 1 = 0 → x + 1 < y + 1 + 1

case succ_succ.mpr
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
⊢ x + 1 < y + 1 + 1 → x + 1 - 1 < y + 1 ∨ x + 1 = 0

State before:
case succ_succ.mp
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
⊢ x + 1 - 1 < y + 1 ∨ x + 1 = 0 → x + 1 < y + 1 + 1
Tactic:
intro
| Or.inl h => exact Nat.succ_lt_succ h
| Or.inr h => absurd h; apply Nat.succ_ne_zero
State after:
no goals

State before:
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
x✝ : x + 1 - 1 < y + 1 ∨ x + 1 = 0
h : x + 1 - 1 < y + 1
⊢ x + 1 < y + 1 + 1
Tactic:
exact Nat.succ_lt_succ h
State after:
no goals

State before:
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
x✝ : x + 1 - 1 < y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ x + 1 < y + 1 + 1
Tactic:
absurd h
State after:
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
x✝ : x + 1 - 1 < y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ ¬x + 1 = 0

State before:
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
x✝ : x + 1 - 1 < y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ ¬x + 1 = 0
Tactic:
apply Nat.succ_ne_zero
State after:
no goals

State before:
case succ_succ.mpr
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
⊢ x + 1 < y + 1 + 1 → x + 1 - 1 < y + 1 ∨ x + 1 = 0
Tactic:
intro h
State after:
case succ_succ.mpr
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
h : x + 1 < y + 1 + 1
⊢ x + 1 - 1 < y + 1 ∨ x + 1 = 0

State before:
case succ_succ.mpr
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
h : x + 1 < y + 1 + 1
⊢ x + 1 - 1 < y + 1 ∨ x + 1 = 0
Tactic:
left
State after:
case succ_succ.mpr.h
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
h : x + 1 < y + 1 + 1
⊢ x + 1 - 1 < y + 1

State before:
case succ_succ.mpr.h
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
h : x + 1 < y + 1 + 1
⊢ x + 1 - 1 < y + 1
Tactic:
exact Nat.lt_of_succ_lt_succ h
State after:
no goals