case on intro

Stream: general

[kana]

Is there a way to split value from intro at once?
I have a lot of such code

intro i,
cases i with f g fg_inv,
cases fg_inv with gf fg,

And I want something like this

intro ⟨f, g, ⟨gf, fg⟩⟩,

Like in ssreflect

move=> [f g [gf fg]]

[Adam Topaz]

tactic#rintro

[Kevin Buzzard]

and ⟨ is right associative so rintro ⟨f, g, gf, fg⟩, should work

[kana]

Oh, but it requires mathlib, and mathlib imports a lot of notations, that conflict with my notations, and it is impossible to hide or disable them.

[Mario Carneiro]

which notations?

[Mario Carneiro]

most mathlib notations are scoped

[kana]

_ᵒᵖ, _ ⟶ _

I am playing with category theory formalization from scratch, and I have such notations

[Kevin Buzzard]

Just import tactic.rcases then

[kana]

Oh thanks, it works. I tried to import the whole tactic

[Kevin Buzzard]

wow, I wonder which tactic needs opposite categories! (but you do seem to be right, one of them does!)

[Adam Topaz]

_ᵒᵖ is used for more than just opposite categories, if I recall correctly... (e.g. the opposite ring, opposite monoid, etc.). I still don't know why importing tactic imports the notation though!

[Adam Topaz]

I bet tactic#transport is a culprit

[Bhavik Mehta]

tactic#op_induction is my guess

[Eric Wieser]

docs#tactic.interactive.op_induction?