How to prove pred_le_pred using tactics

Question

The theorem pred_le_pred is proven in prelude.lean using pattern matching:

theorem Nat.pred_le_pred : {n m : Nat} → LE.le n m → LE.le (pred n) (pred m)
  | _,           _, Nat.le.refl   => Nat.le.refl
  | 0,      succ _, Nat.le.step h => h
  | succ _, succ _, Nat.le.step h => Nat.le_trans (le_succ _) h

I was wondering if there is a way to also prove it using tactics?

Note: this question is about Lean4 and not Lean3

Answer 1

You can use the intro tactic and a match expression to prove the theorem:

namespace Hidden
open Nat

theorem Nat.pred_le_pred : {n m : Nat} → LE.le n m → LE.le (pred n) (pred m) := by
  intro n m h
  match n, m, h with
  | _,           _, Nat.le.refl   => exact Nat.le.refl
  | 0,      succ _, Nat.le.step h => exact h
  | succ _, succ _, Nat.le.step h => exact Nat.le_trans (le_succ _) h

end Hidden

Edit: I've come up with another proof:

namespace Hidden
open Nat

theorem Nat.pred_le_pred : {n m : Nat} → LE.le n m → LE.le (pred n) (pred m) := by
  intro n m h
  cases h
  . exact le.refl
  . rename_i m₁ h₁
    cases n
    . exact h₁
    . rename_i n₁
      exact Nat.le_trans (le_succ n₁) h₁

end Hidden