Simple CovBy result

Stream: Is there code for X?

[Paul Rowe]

I recently found good need for the following result.

import mathlib

variable {α : Type} [SemilatticeSup α]

lemma CovBy.something (a b c : α) (h1 : a ⋖ c) (h2 : b ⋖ c) : a = b ∨ a ⊔ b = c := by
  have sle : a ⊔ b ≤ c := sup_le (CovBy.le h1) (CovBy.le h2)
  cases CovBy.eq_or_eq h1 le_sup_left sle with
  | inl supeq =>
    rw [sup_eq_left, le_iff_eq_or_lt] at supeq
    cases supeq with
    | inl eq => left; exact eq.symm
    | inr lt => exfalso; exact h2.2 lt (h1.1)
  | inr eq => right; exact eq

Is there a close enough variant to this in Mathlib already? If not, would something like this be a good addition to Mathlib (of course once it's better named, and perhaps golfed)?

[Yaël Dillies]

That's an interesting lemma to have, I would say!

[Paul Rowe]

Great! I can make the effort to open a PR. I'm sure the review process will address some of the following issues, but do you have any advice on the following?

• what it should be called
• any improvements in the proof / opportunities to golf
• where it should go (I was thinking perhaps just below docs#CovBy.eq_or_eq)

[Paul Rowe]

Would it be good to also have a variant that has (h3 : ¬a = b) as a hypothesis?

[Ruben Van de Velde]

You could hide the branching a bit:

import Mathlib

variable {α : Type} [SemilatticeSup α]

lemma CovBy.something (a b c : α) (h1 : a ⋖ c) (h2 : b ⋖ c) : a = b ∨ a ⊔ b = c := by
  refine (CovBy.eq_or_eq h1 le_sup_left (sup_le h1.le h2.le)).imp_left fun supeq => ?_
  rw [sup_eq_left, le_iff_eq_or_lt] at supeq
  exact (supeq.resolve_right (h2.2 · h1.lt)).symm

[Ruben Van de Velde]

Or

import Mathlib

variable {α : Type} [SemilatticeSup α]

lemma CovBy.something (a b c : α) (h1 : a ⋖ c) (h2 : b ⋖ c) : a = b ∨ a ⊔ b = c := by
  refine (CovBy.eq_or_eq h1 le_sup_left (sup_le h1.le h2.le)).imp_left fun supeq => ?_
  rw [sup_eq_left] at supeq
  exact supeq.eq_of_not_gt (h2.2 · h1.lt)

[Paul Rowe]

I like it! Thanks!

[Paul Rowe]

In fact, Mathlib already has docs#WCovBy.sup_eq, which is a weak version of the form that takes the disequality as a hypothesis. This could easily be upgraded to a version about strict covers by doing

import mathlib

variable {α : Type} [SemilatticeSup α]

lemma CovBy.sup_eq (a b c : α) (h1 : a ⋖ c) (h2 : b ⋖ c) (h3 : ¬a = b) : a ⊔ b = c :=
    WCovBy.sup_eq (h1.wcovBy) (h2.wcovBy) h3

Do we still think this is a valuable contribution? Is the version with the disjunction in the conclusion worth adding?