Theorem: Nat.le_succ_of_le''' (Fpil/Chap10/Sec04.lean)

State before:
n m : Nat
⊢ n ≤ m → n ≤ succ m
Tactic:
intro h
State after:
n m : Nat
h : n ≤ m
⊢ n ≤ succ m

State before:
n m : Nat
h : n ≤ m
⊢ n ≤ succ m
Tactic:
induction h <;> repeat (first | constructor | assumption)
State after:
no goals

State before:
case step.a.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n m✝
Tactic:
(first | constructor | assumption)
State after:
no goals

State before:
case step.a.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n m✝
Tactic:
first | constructor | assumption
State after:
no goals

State before:
case step.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n (m✝ + 1)
Tactic:
constructor
State after:
case step.a.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n m✝

State before:
case step.a.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n m✝
Tactic:
assumption
State after:
no goals