arguments for `subset_union_left` etc

Stream: mathlib4

[Peter Nelson]

I use the lemmas subset_union_left and the right/intersection versions a huge amount, and I’m getting very tired of parentheses and underscores because of the explicit arguments needed - I nearly always have them as part of a larger term where the arguments can be inferred.
The lattice versions (le_sup_left etc) have implicit arguments. In some cases they can be used instead in long proof terms involving sets, but I have avoided this so far because it feels like defeq abuse.

Would there be support for a PR that introduces primed versions for the four relevant set theorems with implicit parameters?

[Yaël Dillies]

I agree, and I am in fact preparing a PR just for that as we speak

[Yaël Dillies]

(today is "been annoyed for long enough" day)

[Peter Nelson]

Do you mean making them implicit, or primed versions?

[Yaël Dillies]

Making them implicit. The new ( := ) notation means we don't really need a primed version at all.

[Peter Nelson]

This is much more dramatic but has my enthusiastic support!

[Yaël Dillies]

I've opened #13445. It will most definitely not be passing before many rounds of fixes. Please help!

[Richard Osborn]

@Yaël Dillies Taking a look at #13445 unless you've already made more changes?

[Yaël Dillies]

No, go for it!