mathlib newbie issue: exists tactic

Stream: mathlib4

[Colin Gordon]

Hi, I'm not new to theorem proving but am fairly new to Lean and just embarking on my first adventure with mathlib4, and have encountered something surprising:

import Mathlib
theorem mwe : ∃ (x : ℕ), x = 3 :=
  by exists 3; rfl

This code yields an error for "exists 3": tactic 'Lean.Parser.Tactic.existsi' has not been implemented
Since the exists tactic works fine with plan old Lean4, I'm guessing Mathlib overrides the tactic in some way, but I'm having trouble figuring out what to expect here. Am I using the mathlib4 version of exists incorrectly? Am I missing an import? Am I simply not supposed to use "exists" at all, and I should instead just apply Exists.intro (which works)?

Beyond this specific question, where would I expect to find information on this sort of thing? I realize mathlib4 is experimental, etc., and I'm not expecting super-polished documentation or anything, but I'm having trouble figuring out where to start looking for stuff like this.

Thanks in advance.

[Ruben Van de Velde]

There's a fair number of mathlib3 tactics that haven't been implemented yet in mathlib4, but do have their syntax reserved. I'm guessing you ht one of those

[Henrik Böving]

Mathlib is currently overwriting the built in exists syntax here: https://github.com/leanprover-community/mathlib4/blob/1b6c2fbe04b01ab498cf743d2f4725bc1bb3dcfb/Mathlib/Mathport/Syntax.lean#L182 but doesnt provide an elaborator for it yet which causes this error, I'm not entirely sure on the semantics of exists in Lean 3 so maybe there is actually work to be done here or its just a matter of removing this line becaus its a built in by now.

[Ruben Van de Velde]

It might also be worth trying to alias it to use: https://github.com/leanprover-community/mathlib4/blob/1b6c2fbe04b01ab498cf743d2f4725bc1bb3dcfb/Mathlib/Tactic/Use.lean

[Colin Gordon]

Thanks for the explanations and pointers!

[Mario Carneiro]

Note that lean 4 is adding tactics in parallel with mathlib4, and there is often overlap, meaning that it is possible for a new lean 4 version to add support for a tactic that is already on the mathlib 4 todo list (which is almost certainly going to happen unless it's a brand new tactic or the lean 4 devs decided on a different syntax). In this case, we will either scratch it from the mathlib todo list if it's a full implementation, or keep it / add a ' if the mathlib syntax is more generic.

[Mario Carneiro]

In this case, I believe the mathlib syntax is more generic: it accepts "exists" term,+ but the one in lean only accepts "exists" term

[Mario Carneiro]

we could certainly delegate to the lean tactic in the overlap case however

[Mario Carneiro]

I don't think we can alias it to use. use has some known oddities which make it not a complete replacement for existsi, and mathlib in point of fact uses both tactics. If we wanted to remove one or the other, this would have to start as a mathlib refactor

[François G. Dorais]

This has been fixed in core: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Extending.20.60exists.60.3F/near/280133936