feat(order/filter/ultrafilter): add some comap_inf_principal lemmas in the setting of ultrafilters

[berndlosert]

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/contribute.20lemma.20to.20mathlib

Some background: I am developing the theory of convergence spaces in Lean. I need these lemmas in the proof that the image of a compact set under a continuous function is compact.

---

[eric-wieser]

This is just one direction of coe_le_coe on line 53, right? Can you change coe_le_coe to be proved in terms of this lemma?

[berndlosert]

Done.

[jcommelin]

Please update the PR title according to the style guide: https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md

[berndlosert]

I updated the title and the commit.

[PatrickMassot]

@berndlosert could you please move this branch from your fork to the main repository? Out continuous integration workflow requires this in order to be able to check your code before we can make any decision. See explanations at https://leanprover-community.github.io/contribute/index.html. Also please open filter in the section you added so that we can remove all those filter..

[berndlosert]

could you please move this branch from your fork to the main repository?

No problem. I will close this PR and open a new one.

Also please open filter in the section you added so that we can remove all those filter.

I tried doing that already, but Lean gets confused. For example, I get this error when I simply filter.comap to comap:

error: type mismatch at application
  comap m
term
  m
has type
  α → β : Type (max u v)
but is expected to have type
  ultrafilter ?m_1 : Type ?