# How to prove pred_le_pred using tactics

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

• It's not necessary to include the prover in the title, because people can see it in the tags, and this saves up more space to display more important parts of your title :)
– Trebor
Mar 7 at 9:15
• It's always possible to prove term-mode things using tactics; exact <the_term> for one example. You should look into the cases tactic, which may be closer to what you want. Mar 7 at 10:56
• Yes I can use exact, but I would like to know how to try different tactics as I am trying to reason and figure out how to prove this theorem. I have tried cases and induction without success. Mar 7 at 15:29

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

• What I want to know is how to do with without any expressions and only using tactics, since it is hard to partially prove things using expressions. Mar 7 at 15:28
• @WalterSchulze I've just added another proof to my answer. Mar 8 at 5:28
• Amazing yes thank you. The key was to do cases on n ≤ m Mar 8 at 11:28