Theorem: nat_pred_le_pred (Katydid/Std/Lists.lean)

State before:
⊢ ∀ {n m : ℕ}, n ≤ m → pred n ≤ pred m
Tactic:
intro n m h
State after:
n m : ℕ
h : n ≤ m
⊢ pred n ≤ pred m

State before:
n m : ℕ
h : n ≤ m
⊢ pred n ≤ pred m
Tactic:
cases h with
| refl => constructor
| step h =>
  rename_i m
  cases n with
  | zero =>
    dsimp
    exact h
  | succ n =>
    dsimp
    have h_n_le_succ_n := Nat.le_succ n
    exact (Nat.le_trans h_n_le_succ_n h)
State after:
no goals

State before:
case refl
n : ℕ
⊢ pred n ≤ pred n
Tactic:
constructor
State after:
no goals

State before:
case step
n m✝ : ℕ
h : Nat.le n m✝
⊢ pred n ≤ pred (succ m✝)
Tactic:
rename_i m
State after:
case step
n m : ℕ
h : Nat.le n m
⊢ pred n ≤ pred (succ m)

State before:
case step
n m : ℕ
h : Nat.le n m
⊢ pred n ≤ pred (succ m)
Tactic:
cases n with
| zero =>
  dsimp
  exact h
| succ n =>
  dsimp
  have h_n_le_succ_n := Nat.le_succ n
  exact (Nat.le_trans h_n_le_succ_n h)
State after:
no goals

State before:
case step.zero
m : ℕ
h : Nat.le zero m
⊢ pred zero ≤ pred (succ m)
Tactic:
dsimp
State after:
case step.zero
m : ℕ
h : Nat.le zero m
⊢ 0 ≤ m

State before:
case step.zero
m : ℕ
h : Nat.le zero m
⊢ 0 ≤ m
Tactic:
exact h
State after:
no goals

State before:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
⊢ pred (succ n) ≤ pred (succ m)
Tactic:
dsimp
State after:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
⊢ n ≤ m

State before:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
⊢ n ≤ m
Tactic:
have h_n_le_succ_n := Nat.le_succ n
State after:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
h_n_le_succ_n : n ≤ succ n
⊢ n ≤ m

State before:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
h_n_le_succ_n : n ≤ succ n
⊢ n ≤ m
Tactic:
exact (Nat.le_trans h_n_le_succ_n h)
State after:
no goals