feat(tactic/ext): add apply_cfg argument to ext1

[semorrison]

This causes goals to appear in the same order they appear as hypotheses of the
@[extensionality] lemma, rather than being reordered to put dependent
goals first.

This doesn't appear to affect any uses of ext in mathlib,
but is occasionally helpful in the development of category theory.

(Indeed, I have been running into tactic mode proofs that fail to
typecheck, when using ext, and this avoids the problem. My
actual dependent ext lemma is at here, and the place where I need
to swap the goals back into order by hand is here.)

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean

For reviewers: code review check list

[digama0]

I think you should add a configuration option rather than changing the default.

[semorrison]

I added an optional apply_cfg argument, just to the non-interactive tactic. I also added a short wrapper in tidy, that decides whether to just report ext or also report passing a configuration. This logic could be further improved, perhaps.

[semorrison]

Perhaps in Lean 4 we can discuss the best default value for apply_cfg.new_goals!