[Merged by Bors] - chore(data/finsupp/basic): make arguments explicit

[eric-wieser]

This follow the pattern that arguments to an = lemma should be explicit if they're not implied by other arguments.

---

[fpvandoorn]

I don't think this is a rule at all. There are many examples where it's more convenient to have it implicit. See e.g. closure_closure or closure_union.

Is there a single occurrence of @foo or (foo : ...) you could simplify using these changes?

[eric-wieser]

I'd argue that the arguments should be explicit in your two examples too; it's a lot harder to target a specific rewrite if you can't fill out any of the unbound variables.

[fpvandoorn]

Maybe you're right.
I think it's a lot more common that you want arguments to non-equalities to be implicit (I'm annoyed that lemmas like subset_union_(left|right) have explicit arguments), but I guess the difference is that you cannot rw with ⊆, and therefore you write term-mode proofs way more frequently than with =. This is rarely a problem with equality proofs.

bors merge

[bors]

👎 Rejected by label

[fpvandoorn]

good bot

bors d+

[bors]

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

Yes, I agree that non-equalities typically have different rules.

[eric-wieser]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests