Can this be golfed?

Stream: Is there code for X?

[Antoine Chambert-Loir]

I wrote this for #23993 and I wonder whether it can be made shorter.

import Mathlib.Algebra.Order.Monoid.Unbundled.Basic

@[to_additive]
theorem trichotomy_of_mul_eq_mul {α : Type*} [LinearOrder α] [Mul α]
    [MulLeftMono α] [MulLeftStrictMono α] [MulRightMono α] [MulRightStrictMono α]
    {a b c d : α}  (h : a * b = c * d) :
    (a = c ∧ b = d) ∨ (a < c ∨ b < d) := by
  by_cases hac : a < c
  · right; left; exact hac
  · by_cases hbd : b < d
    · right; right; exact hbd
    · left
      simp only [not_lt] at hac hbd
      by_contra h'
      apply ne_of_lt _ h.symm
      rw [not_and_or] at h'
      rcases h' with h' | h'
      · exact mul_lt_mul_of_lt_of_le (lt_of_le_of_ne hac (Ne.symm h')) hbd
      · exact mul_lt_mul_of_le_of_lt hac (lt_of_le_of_ne hbd (Ne.symm h'))

[Kevin Buzzard]

This doesn't compile for me, even after adding import Mathlib and (a b c d : α).

[Antoine Chambert-Loir]

bad copy paste, I'm sorry.

[Kevin Buzzard]

Under your assumptions on alpha, are a * b = a * d -> b = d and a * b = c * d -> c < a -> b < d true and missing?

[Antoine Chambert-Loir]

I just tried that in the sandbox. (and the PR compiles).

[Kevin Buzzard]

Usually I would go for obtain hac | rfl | hca := lt_trichotomy a c rather than by_cases on an < (which gives you \not < in the other case, which is almost always not what you want). Even if you want to split into a < b or b <= a you can do obtain h1 | h2 := lt_or_le a b

[Kevin Buzzard]

But then you run into these two missing lemmas which I flagged above.

[Edison Xie]

Antoine Chambert-Loir said:

  · right; left; exact hac

this is just tauto

[Antoine Chambert-Loir]

I hadn't thought about tauto, but it doesn't yet exist in these early files.

[Edison Xie]

Ah okay but it's a easy hack for · right; right; exact hbd as well :joy:

[Edison Xie]

combining @Kevin Buzzard 's suggestion gives:

import Mathlib

@[to_additive]
theorem trichotomy_of_mul_eq_mul {α : Type*} [LinearOrder α] [Mul α]
    [MulLeftMono α] [MulLeftStrictMono α] [MulRightMono α] [MulRightStrictMono α]
    {a b c d : α}  (h : a * b = c * d) :
    (a = c ∧ b = d) ∨ (a < c ∨ b < d) := by
  obtain hac | rfl | hca := lt_trichotomy a c
  · tauto
  · left; simpa using mul_right_inj_of_comparable (LinearOrder.le_total d b)|>.1 h
  · right; right; by_contra! h'; exact (ne_of_lt (mul_lt_mul_of_lt_of_le hca h')) h.symm