intros equivalent

Stream: mathlib4

[Yaël Dillies]

Is there an equivalent of intros called without arguments somewhere? If there's nothing to introduce, intro complains with

tactic 'introN' failed, insufficient number of binders

[Thomas Murrills]

I might be mistaken but I believe intros called without arguments is, well, intros called without arguments? :grinning_face_with_smiling_eyes: (Stuck building atm, can't check)

[Thomas Murrills]

Or, wait—do you mean something that behaves like intro when there is something to introduce but intros when there isn't?

[Thomas Murrills]

(In which case, does try intro work?)

[Eric Rodriguez]

intros introduces "all" the arguments (for some definition of all) when you don't pass any arguments to it

[Thomas Murrills]

Right, so isn't that "intros, but without arguments"? I must be misunderstanding—what's the desired behavior?

[Yaël Dillies]

Does intros still exist? It wasn't recognized as an identifier.

[Thomas Murrills]

Hmm, it does, and it behaves the way you're expecting it to. What's the context where it's not recognized?

[Yaël Dillies]

You can try things out in !4#2911. Compare with the proof of docs#ulift.division_semiring

[Thomas Murrills]

The following works just fine for me:

instance divisionSemiring [DivisionSemiring α] : DivisionSemiring (ULift α) := by
  refine' down_injective.divisionSemiring down _ _ _ _ _ _ _ _ _ _ <;> intros <;> rfl

[Yaël Dillies]

Okay, I don't know what I've done!

[Thomas Murrills]

Or, more compactly:

instance divisionSemiring [DivisionSemiring α] : DivisionSemiring (ULift α) := by
  refine' down_injective.divisionSemiring down .. <;> intros <;> rfl

[Thomas Murrills]

Ohh, based on the error, here's one possibility: maybe one in that extremely long string of underscores got lost, and then intros tried to be interpreted as a term instead of a tactic. If I delete an underscore and the punctuation, that's what happens!

[Yaël Dillies]

Oh, that's quite a confusing error message then!