Unravelling notations in Lean

Question

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
  rw [HAdd.hAdd]
  unfold instHAdd
  simp
  rw [Add.add]
  unfold instAddNat

My Tactic state is then

nm: Nat
⊢ { add := Nat.add }.1 (succ n) m = succ ({ add := Nat.add }.1 n m)

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?

Answer 1

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
  induction m <;> simp_all [Nat.add_succ]

This theorem already exists as Nat.succ_add by the way.