viewing an expanded term

Stream: Is there code for X?

[Octavian-Mircea Sebe]

Hi!
I'm just learning Lean and I was wondering if there is any way to view the reduced form of a term with definitions expanded, while inside the proof, without having to copy it and paste it inside a #reduce outside of my proof?
That would be a very convenient feature to have.
And sorry in advance if this is a stupid question but I couldn't find any mention of that anywhere on the web or docs.

[Kyle Miller]

I'm not sure I have a good answer for this, but what I usually do is simp only [names, of, definitions, I, want, to, expand].

There's also simp!

[Patrick Massot]

This is much less useful than you think it is (unless you plan to make a very specific exotic use of Lean).

[Octavian-Mircea Sebe]

Patrick Massot said:

This is much less useful than you think it is (unless you plan to make a very specific exotic use of Lean).

I was doing the Lean tutorial and at some point I had a hypothesis of type seq_limit u l and I didn't want to have to look up the definition of seq_limit to know what tactic to use next.

[Yakov Pechersky]

You can always click on the term in the goal view, will show a widget with more information, including what the term is constructed from, and links to the definition

[Kevin Buzzard]

What you do next doesn't depend on the definition of seq_limit, it depends on the next mathematical step and would require knowing the API for the definition rather than the internal implementation, right?

[Octavian-Mircea Sebe]

Kevin Buzzard said:

What you do next doesn't depend on the definition of seq_limit, it depends on the next mathematical step and would require knowing the API for the definition rather than the internal implementation, right?

So what would be the API for the definition in this case?

[Kyle Miller]

@Kevin Buzzard In the tutorial the definition is the API

[Kevin Buzzard]

Oh! In which case maybe unfold seq_limit is what you're looking for?

[Patrick Massot]

Or right-click on the word in the edit buffer and then "Peek definition"