nat.rec_succ

Stream: Is there code for X?

[Eric Wieser]

Is this builtin to mathlib or lean somewhere?

lemma rec_succ {C: ℕ → Type} {zero_f : C 0} {succ_f : Π n, C n → C n.succ} {n : ℕ} :
  @nat.rec C zero_f succ_f (n + 1) = succ_f n (@nat.rec C zero_f succ_f n) := rfl

In general, it seems like if I have an inductive rec operating on a object of a known constuctor, I should be able to unfold it one level.

[Eric Wieser]

( I needed this for a proof about a deliberately awkward def in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/recursive.20let.20in/near/209644962)

[Reid Barton]

This is the L rule for some Greek letter L

[Reid Barton]

dsimp should apply it for example

[Eric Wieser]

Ahh, there's a hidden nat.add_one that I also needed