# Unravelling notations in Lean

When one is busy writing a proof in Lean, one sometimes encounters symbols, like + or <=, but one does not know what the underlying function name and instance function name is. How does one go about unfolding a symbol. This is useful if you want to do simp or rw on that function.

Is there a way to use tactics to get the underlying function, for example to know that + is, I had to guess to do rw [HAdd.hAdd], I did not find it, I just remembered that H is sometimes prefixed.

Now I can write:

theorem nat_add_succ_is_succ_add (n m: Nat):
succ n + m = succ (n + m) := by
simp


My Tactic state is then

nm: Nat


This seems like a long way to go and also I didn't know how to find HAdd.hAdd. Is there a more efficient way and how does one go about finding HAdd.hAdd or can we skip this altogether using some other command or tactic?

I would also like to unfold my Tactic state to the point that I get:

Nat.add (succ n) m = succ (Nat.add n m)


But simp takes me back to +.

Is there a way to bring my Tactic state to this state?

• simp only to answer your specific question at the end. Mar 10 at 15:51
• And usually clicking on things in the tactic state (using widgets) is the quick way to identify what the head symbol actually is. Mar 10 at 15:52
• Mar 10 at 17:24

You don't need to know what + is short for if you use simp.

  simp only [(· + ·), Add.add]
-- new goal: ⊢ Nat.add (succ n) m = succ (Nat.add n m)


Here I simply typed out the functions I saw in the info view. I used simp only to avoid the global simp lemma Nat.add_eq, which as you said would bring us back to +.

Now, why does that simp lemma exist? Because we want to make sure that we don't end up with goals using a mixture of abstract + and concrete functions like Nat.add, which could complicate applying further lemmas to them, i.e. + is considered the "canonical form" of Nat.add. Nat.add_succ is an example of such a lemma stated in terms of +, and so we can do the proof without ever unfolding +.

theorem nat_add_succ_is_succ_add2 (n m : Nat) :
succ n + m = succ (n + m) := by

This theorem already exists as Nat.succ_add by the way.
• simp only [(· + ·), Add.add] is pretty great, but how would one do a rw [(· + ·)] ? Mar 12 at 13:51
• rw doesn't know about that syntax. It is essentially a dumber simp, so it's expected to do less, though whether this particular feature should be supported is a good question. Mar 12 at 17:27
• I was assuming that the syntax for (· + ·) was a general syntax that could be used with rewrite, unfold or anywhere where you would want to reference the + function in a tactic. Mar 13 at 10:34