Prod.Lex.lt_of_le_of_lt

Stream: Is there code for X?

[Violeta Hernández]

I feel like I've asked for this before, but I can't find it.

[Violeta Hernández]

Basically, I want a ≤ c → b < d → (a, b) < (c, d)

[Kim Morrison]

import Mathlib

example {α} [LinearOrder α] (a b c d : α) : a ≤ c → b < d → (a, b) < (c, d) := by
  intros h1 h2
  exact?

[Kim Morrison]

When asking for something that you're sure must be there, I think a good strategy is to post the by exact? command that fails. Or, in many cases, such as this one, discover that it in fact succeeds, and you don't need to ask. :-)

[Notification Bot]

Violeta Hernández has marked this topic as resolved.

[Violeta Hernández]

Wait no, that's not the correct lemma

[Notification Bot]

Violeta Hernández has marked this topic as unresolved.

[Violeta Hernández]

What I actually want is:

import Mathlib

example {α} [LinearOrder α] (a b c d : α) : a ≤ c → b < d → toLex (a, b) < toLex (c, d) := by
  intros h1 h2
  exact?

And here exact? comes up with nothing

[Violeta Hernández]

theorem Prod.Lex.lt_of_le_of_lt {α β} [PartialOrder α] [LT β] {a b : α} {c d : β}
    (h₁ : a ≤ b) (h₂ : c < d) : toLex (a, c) < toLex (b, d) := by
  obtain h₁ | rfl := h₁.lt_or_eq
  · exact Prod.Lex.left _ _ h₁
  · exact Prod.Lex.right _ h₂

[Violeta Hernández]

This is a huge deja-vu... I swear I've asked this before?

[Violeta Hernández]

I guess I'd also like to mention that when faced with a goal of the form toLex (a, b) < toLex (c, d), decreasing_tactic eagerly reduces this to a < c which isn't necessarily true

[Violeta Hernández]

#18484

[Yaël Dillies]

docs#Prod.Lex.toLex_strictMono

[Violeta Hernández]

I see

[Violeta Hernández]

I still think we should have this specific instance of the theorem

[Violeta Hernández]

Or otherwise I'll just ask about it again two months from now :zany_face:

[Violeta Hernández]

Violeta Hernández said:

theorem Prod.Lex.lt_of_le_of_lt {α β} [PartialOrder α] [LT β] {a b : α} {c d : β}
    (h₁ : a ≤ b) (h₂ : c < d) : toLex (a, c) < toLex (b, d) := by
  obtain h₁ | rfl := h₁.lt_or_eq
  · exact Prod.Lex.left _ _ h₁
  · exact Prod.Lex.right _ h₂

This version only assumes LT beta rather than Preorder beta, but maybe that same change can be made to the StrictMono lemma

[Violeta Hernández]

Not like it matters much anyways

[Yaël Dillies]

No sorry I think we really should channel these kinds of arguments through Prod.Lex.toLex_mono and Prod.Lex.toLex_strictMono

[Yaël Dillies]

... if only because I don't want a ton of versions for (a, b, c) < (d, e, f)

[Violeta Hernández]

If so, could we document this approach somewhere?

[Violeta Hernández]

My first instinct when proving an inequality involving lexicographic ordering isn't usually "the type alias map between these two different kinds of product orderings is strictly monotonic"