Bugs in `ext` tactic

[fgdorais]

These bugs were noticed in the discussion of #611.

The .ext and .ext_iff lemmas generated by applying the @[ext] attribute to a structure has sub-optimal binders. For example:

@[ext] structure S (α β) where (a : α) (b : β)
/-
S.ext.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (x y : S α β) (a : x.a = y.a) (b : x.b = y.b) : x = y
-/
#check S.ext

One would expect x y to be implicit parameters.

The @[local ext]/@[scoped ext] variants don't work correctly when applied to structures.

• The generated .ext lemma is marked plain @[ext] instead of @[local ext]/@[scoped ext].
• The .ext and .ext_iff are unconditionally generated, which fails if the lemmas were already generated by an unrelated @[local ext] in a a dependency, for example.

[fgdorais]

After a bit of scouting, a better implementation should make use of these tools from core Lean.Meta.CongrTheorems.

I'm willing to do this but since my Lean time is limited it could take a long time.

[fgdorais]

Migrated to lean4#3643