Proving Equivalence with Subtraction

Question

I am in the process of learning Lean, and am working through a very simple example:

def toFin6 (n:Nat) : Fin 6 :=
  if p:n < 6 then { val := n, isLt := by exact p2 }
  else
    toFin6 (n - 1)
  decreasing_by
    simp_wf
    induction n
    /- n = 0 -/
    contradiction
    /- n > 0 -/
    sorry

I appreciate there are simpler ways of converting a Nat into a Fin X type. But, that's not the point. I'm stuck here, where the goal is effectively this:

theorem p (n:Nat) : Nat.succ n - 1 == n :=
by 
  sorry

Logically, it seems straightforward: (n+1)-1 == n. Also, I'm aware that I can resolve this as follows:

import Mathlib.Tactic.Linarith

theorem p (n:Nat) : Nat.succ n - 1 == n :=
by 
  simp

Ok, but how to do it without simp and just using basic tactics in the Prelude? Seems like Nat.succ_sub_one could be useful here.

Answer 1

Ok, so I did come up with this eventually:

theorem p (n:Nat) : Nat.succ n - 1 = n :=
by
  rw [Nat.succ_sub_succ]
  rw [Nat.sub_zero]

It was only via the VS code completion that I found those tactics. Is there a list of them somewhere?