Does "have" work in Lean4

Stream: lean4

[James Caldwell]

I'm looking for a tactic that allows me to make an assertion - a cut tactic. Seems like "have" is not a tactic - must be something similar.

[Mario Carneiro]

it is a tactic and a term

[Mario Carneiro]

the answer to your question is have

[James Caldwell]

OK - thanks. I hate being so dense.

[Martin Dvořák]

I prefer the tactic have that comes from Mathlib.Tactic.Have which is afaik different from the one in the core.

[Mario Carneiro]

the have from mathlib is an addition to the one from core, it doesn't do anything to the original

[Mario Carneiro]

the original is have : ty := e or have : ty := by tac, the one from mathlib is have : ty which produces a subgoal which can be proved by . tac

[Martin Dvořák]

Can I use the new have with a proof term without writing exact please?

[Mario Carneiro]

that's have : ty := e

[Mario Carneiro]

you don't need mathlib for that

[Martin Dvořák]

I mean, if the Mathlib's have is imported, does the := notation still work?

[Mario Carneiro]

Mario Carneiro said:

the have from mathlib is an addition to the one from core, it doesn't do anything to the original

[Martin Dvořák]

You mean; the elaborator automatically finds out which of them I am using?

[Mario Carneiro]

They are different tactics with different syntax. (Unlike lean 3, in lean 4 the whole tactic parse can be used to distinguish different tactics. They don't have to start with unique words; this is only conventional.)

[Mario Carneiro]

the mathlib tactic has the syntax "have" name? [: expr]? while the lean tactic has the syntax "have" name? [: expr?] := expr