WithTop.coe_iSup or WithTop.coe_ciSup

Stream: mathlib4

[Joachim Breitner]

We currently have

theorem WithTop.coe_iSup [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) :
    ↑(⨆ i, f i) = (⨆ i, f i : WithTop α)

and in a project of mine I felt the need to defined

theorem WithBot.coe_iSup_OrderTop {ι : Type*} [Nonempty ι] [SupSet α] [OrderTop α] {f : ι → α} :
    ↑(⨆ i, f i) = (⨆ i, f i : WithBot α) :=
  WithBot.coe_iSup (OrderTop.bddAbove (Set.range f))

which I was about to PR.

Based on the docs at https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/ConditionallyCompleteLattice/Basic.html which state

To differentiate the statements between complete lattices and conditionally complete lattices, we prefix sInf and sSup in the statements by c, giving csInf and csSup. For instance, sInf_le is a statement in complete lattices ensuring sInf s ≤ x, while csInf_le is the same statement in conditionally complete lattices with an additional assumption that s is bounded below.

So it seems that the existing WithTop.coe_iSup should be called WithTop.coe_ciSup, and my lemma should be WithTop.coe_iSup? Or am I missing something here?

[Joachim Breitner]

Ah, there is a :thumbs_up: I guess that means that I’m not wrong, and that therefore this PR is helpful?
https://github.com/leanprover-community/mathlib4/pull/15560

Yuck

::ERR file=Mathlib/Order/ConditionallyCompleteLattice/Basic.lean,line=1,code=ERR_NUM_LIN::Mathlib/Order/ConditionallyCompleteLattice/Basic.lean:1 ERR_NUM_LIN: file contains 1705 lines (at most 1700 allowed), try to split it up

I don’t feel confident enough about mathlib to make a judgement call on how to split this up.

[Damiano Testa]

This is the "common" use-case and you should feel completely entitled to add a linter exception to silence the linter!

[Damiano Testa]

There has been much talk of making the linter suggest to add the exception more prominently, but I am not sure what the status of that change is.