Tactic

Stream: mathlib4

[Suvendu Kar]

I am getting the following error while using "intros a b " in Lean 4:: 'introN' failed, insufficient number of binders
Kindly tell how to resolve it.

[Jireh Loreaux]

It seems like you are trying to introduce more variables than are available in your goal state, but you need to provide a #mwe in order for us to give you better answers.