Theorem: nat_pred_le_succ' (Katydid/Std/Lists.lean)

State before:
⊢ ∀ {n m : ℕ}, Nat.le n (succ m) → Nat.le (pred n) m
Tactic:
intro n m h
State after:
n m : ℕ
h : Nat.le n (succ m)
⊢ Nat.le (pred n) m

State before:
n m : ℕ
h : Nat.le n (succ m)
⊢ Nat.le (pred n) m
Tactic:
cases h with
| refl =>
  constructor
| step h =>
  cases n with
  | zero =>
    dsimp only [zero_eq, Nat.pred_zero, le_eq]
    exact h
  | succ n =>
    dsimp only [Nat.pred_succ, le_eq]
    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
m : ℕ
⊢ Nat.le (pred (succ m)) m
Tactic:
constructor
State after:
no goals

State before:
case step
n m : ℕ
h : Nat.le n m
⊢ Nat.le (pred n) m
Tactic:
cases n with
| zero =>
  dsimp only [zero_eq, Nat.pred_zero, le_eq]
  exact h
| succ n =>
  dsimp only [Nat.pred_succ, le_eq]
  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
⊢ Nat.le (pred zero) m
Tactic:
dsimp only [zero_eq, Nat.pred_zero, le_eq]
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
⊢ Nat.le (pred (succ n)) m
Tactic:
dsimp only [Nat.pred_succ, le_eq]
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