Specialized `ext` lemmas

Stream: general

[Yury G. Kudryashov]

Would it be hard to make ext use more information to match lemmas? There are (in mathlib or not yet) specialized ext lemmas for (additive/multiplicative/linear/ring/algebra) homomorphisms from nat, int, submodule.quotient, monoid_algebra, finsupp=direct_sum, multiset, free_*.

[Yury G. Kudryashov]

Now I'm adding *hom_ext lemmas and applying them explicitly.

[Yury G. Kudryashov]

I'm talking about, e.g., (f g : free_group α →* G) (h : ∀ x : α, f (of x) = g (of x)) : f = g or (f g : nat →+ A) (h : f 1 = g 1) : f = g, or (p : submodule R M) (f g : p.quotient →ₗ[R] M₂) (h : ∀ x : M, f (quotient.mk x) = g (quotient.mk x)) : f = g.

[Yury G. Kudryashov]

We can use ext ⟨x⟩ instead of the last one but not for the other lemmas.

[Yury G. Kudryashov]

A few more: (f g : (α →₀ A) →+ B) (h : ∀ a b, f (single a b) = g (single a b)) : f = g, (f g : monoid_algebra k G →ₐ[k] A) (h : ∀ a, f (single a 1) = g (single a 1)) : f = g.

[Yury G. Kudryashov]

Another possibility: make ext aware of priority and make all these lemmas have higher priority than generic ones. If the top-priority lemma fails, ext should try the next one.

[Kevin Buzzard]

Is it clear what someone wants ext to do in practice? Do they always want the most aggressive one?

[Reid Barton]

I wouldn't be surprised if ext was automatically aware of priority; did you try it?

[Reid Barton]

I think I remember @Floris van Doorn saying that some kind of enumerating over declarations with a given tag orders by priority by default

[Floris van Doorn]

The tactic attribute.get_instances returns a list ordered by priority, the first element has the highest priority. If priorities are tied then it depends on when a declaration is given (and probably the order in which you import files).

[Yury G. Kudryashov]

Thank you. I forgot to post here that I've tried adding extra @[ext] attributes and it worked. I'll PR some of those @[ext]s.