[Merged by Bors] - feat(order/complete_lattice): missing API lemmas about the prod instance

[eric-wieser]

This adds lemmas about how fst, snd, and swap interact with Sup and Inf.

---

[alreadydone]

LGTM, Thanks! Is there a mathlib4 PR?

[eric-wieser]

No, I haven't made a mathlib4 PR because I don't know how to use mathport to generate the Lean4 version, and I don't really want to port manually.

Should I just put the lemmas in order/hom/complete_lattice instead with a TODO to move them after the port?

[alreadydone]

@eric-wieser Have you figured out how to use mathport oneshot (I saw you asked on Zulip)? CI is now reporting a timeout in an unrelated file, so some speedups are in order.

[eric-wieser]

I did a rebase in the hope it would make the seemingly unrelated timeout go away.

I haven't had a chance to try mathport yet.

[alreadydone]

Should I just put the lemmas in order/hom/complete_lattice instead with a TODO to move them after the port?

I think you can do that, but we'd better keep track of where they should be moved, and there are two blocks of lemmas ... In any case, I think #18023 is good as is and could be merged without waiting for this; what do you think?

[mans0954]

I had a go at doing a manual port as an exercise in familiarising myself with the new syntax.

The only problem is that simp_rw can no longer prove swap_infᵢ and swap_supᵢ.

[YaelDillies]

I would make has_Sup and has_Inf sections to clear up the statements, but else this looks good. I cannot see anything obvious missing.

[eric-wieser]

I'd argue it's perhaps better to keep each sup lemma next to its inf lemma, as that makes it easier to spot that they are in sync. I think we alternate between your approach and my one in different places in mathlib.

[YaelDillies]

Sure it doesn't matter that much.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[ocfnash]

@eric-wieser Is there now a corresponding Mathlib4 PR or does this comment still apply?

[eric-wieser]

There is a mathlib 4 PR, but my intent is to discard it and replace it with the output of mathport one this one is merged.

[ocfnash]

bors merge

[bors]

Build failed (retrying...):

• Run tests

[Vierkantor]

In case the build fails:

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.

[bors]

Pull request successfully merged into master.

Build succeeded:

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

[YaelDillies]

Oh I'm only noticing now, but maybe this statement is better?

lemma swap_Inf [has_Inf α] [has_Inf β] (s : set (α × β)) : (Inf s).swap = Inf (prod.swap ⁻¹' s) :=

[eric-wieser]

I don't really need this lemma anyway, I was just listing every trivial function it could interact with. Feel free to make a PR to spell it that way instead.