Monotone Prod.fst for Lex products

Stream: Is there code for X?

[Scott Carnahan]

I was hoping to prove something like the following:

import Mathlib.Data.Prod.Lex

theorem monotone_prod_fst_lex [PartialOrder α] [PartialOrder β] (t c: (α ×ₗ β)) (h : t ≤ c) :
    t.1 ≤ c.1 := by
  sorry

Using refine Monotone.imp ?_ h reduces the goal to Monotone Prod.fst, but my usual methods are leading me into circles here.

[Ruben Van de Velde]

Probably something with docs#Prod.Lex.le_iff

[Scott Carnahan]

theorem monotone_prod_fst_lex [PartialOrder α] [PartialOrder β] (t c: (α ×ₗ β)) (h : t ≤ c) :
    t.1 ≤ c.1 := by
  cases ((Prod.Lex.le_iff t c).mp h) with
  | inl h' => exact LT.lt.le h'
  | inr h' => simp_all only [le_refl]

[Scott Carnahan]

Thank you!

[Eric Wieser]

Strictly speaking that statement is ill-typed; it should mention ofLex before using .1