Goal equal to hypothesis (fuction expected)

Stream: new members

[Andrés Goens]

Hi,

I'm trying to prove something for which I got (via some rewrites) the goal as an hypothesis p. When I tell Lean to close it with exact p, it tells me it expects a function, but I don't understand why. Does anyone have a clue what might be happening? A bit more concretely, my proof state looks something like:

...
p : l₁ ~ l₂
...
⊢ l₁ ~ l₂

And I get the error:

function expected at
  p
term has type
  l₁ ~ l₂

Why does exact expect a function? I thought it should expect (a witness of) the proof of the goal, which is what I'm giving it.

Just in case that matters, this is with Lean4 (version 4.0.0-m2, commit 26dda3f63d88, to use Mathlib4)

[Ruben Van de Velde]

Can you post a #mwe?

[Ruben Van de Velde]

(Not that I have a clue about lean4)

[Ruben Van de Velde]

There isn't anything left after the exact p? That sometimes catches me out in lean3

[Andrés Goens]

What do you mean anything left? The exact p fails with that error. I'll try to construct a #mwe

[Jakob von Raumer]

You could precede the theorem with set_option pp.all true in to get more info from the output, maybe there's a wrong implicit argument or type class instance in p.

[Andrés Goens]

That seems like a useful tool for debugging, thanks :) It seems there isn't a wrong implicit argument there:

p : @List.perm.{u_1} α l₁ l₂
...
⊢ @List.perm.{u_1} α l₁ l₂

[Jakob von Raumer]

What does the line before the exact p look like?

[Andrés Goens]

Hm, the problem somehow disappeared when trying to construct a #mwe and I don't know exactly why. I think Lean accepted my exact and was complaining about what is afterwards? Now it says goals accomplished and I have no idea what changed... Sorry for the confusion and thanks for the help!

[Jakob von Raumer]

It was probably more something about the sequences of tactics, that confused the parser. Maybe indentation?

[Andrés Goens]

Indentation matters in Lean? That sounds like a very plausible suspect! Do you know if how indentation works is documented somewhere?

[Jakob von Raumer]

Yes, it does in Lean 4. Because we don't have tactic blocks scoped by begin ... end anymore