golfing contest

Stream: general

[Damiano Testa]

Dear All,

I feel that my proof below is very clumsy: does anyone have a better proof of the lemma?

Thanks!

import algebra.order.monoid


@[to_additive] lemma eq_and_eq_of_le_of_le_of_mul_eq {A} [has_mul A] [linear_order A]
  [covariant_class A A (*) (≤)] [covariant_class A A (function.swap (*)) (<)]
  [contravariant_class A A (*) (≤)]
  {a b a0 b0 : A} (ha : a0 ≤ a) (hb : b0 ≤ b) (ab : a * b = a0 * b0) :
  a = a0 ∧ b = b0 :=
begin
-- im-prove me, please!
  rcases trichotomous_of (<) a a0 with h | rfl | h,
  { exact (lt_irrefl _ (h.trans_le ha)).elim },
  { refine ⟨rfl, _⟩,
    rcases trichotomous_of (<) b b0 with h | rfl | h,
    { exact (lt_irrefl _ (h.trans_le hb)).elim },
    { refl },
    { exact le_antisymm (le_of_mul_le_mul_left' ab.le) ‹_› } },
  { exact (lt_irrefl _ ((mul_lt_mul_of_lt_of_le h hb).trans_le ab.le)).elim }
end

[Ruben Van de Velde]

Slightly improved:

import algebra.order.monoid

@[to_additive] lemma eq_and_eq_of_le_of_le_of_mul_eq {A} [has_mul A] [linear_order A]
  [covariant_class A A (*) (≤)] [covariant_class A A (function.swap (*)) (<)]
  [contravariant_class A A (*) (≤)]
  {a b a0 b0 : A} (ha : a0 ≤ a) (hb : b0 ≤ b) (ab : a * b = a0 * b0) :
  a = a0 ∧ b = b0 :=
begin
  obtain rfl|h := ha.eq_or_lt,
  { refine ⟨rfl, _⟩,
    obtain rfl|h := hb.eq_or_lt,
    { refl },
    { exact le_antisymm (le_of_mul_le_mul_left' ab.le) ‹_› } },
  { exact (lt_irrefl _ ((mul_lt_mul_of_lt_of_le h hb).trans_le ab.le)).elim }
end

[Damiano Testa]

Thanks!

This also works, but, given the statement, it also feels very awkward:

@[to_additive] lemma eq_and_eq_of_le_of_le_of_mul_eq {A} [has_mul A] [linear_order A]
  [covariant_class A A (*) (≤)] [covariant_class A A (function.swap (*)) (<)]
  [contravariant_class A A (*) (≤)]
  {a b a0 b0 : A} (ha : a0 ≤ a) (hb : b0 ≤ b) (ab : a * b = a0 * b0) :
  a = a0 ∧ b = b0 :=
begin
  haveI : covariant_class A A (function.swap (*)) (≤) := has_mul.to_covariant_class_right A,
  contrapose! ab,
  refine ((mul_le_mul' ha hb).lt_of_ne _).ne',
  rcases eq_or_ne a a0 with rfl | ha0,
  refine (_root_.mul_lt_mul_left' (hb.lt_of_ne (ab rfl).symm) _).ne,
  exact (mul_lt_mul_of_lt_of_le (lt_of_le_of_ne ha ha0.symm) hb).ne,
end

[FR]

@[to_additive] lemma eq_and_eq_of_le_of_le_of_mul_eq {A} [has_mul A] [linear_order A]
  [covariant_class A A (*) (≤)] [covariant_class A A (function.swap (*)) (<)]
  [contravariant_class A A (*) (≤)]
  {a b a0 b0 : A} (ha : a0 ≤ a) (hb : b0 ≤ b) (ab : a * b = a0 * b0) :
  a = a0 ∧ b = b0 :=
begin
  haveI := has_mul.to_covariant_class_right A,
  have ha' : a0 < a → a0 * b0 < a * b := λ h, mul_lt_mul_of_lt_of_le h hb,
  have hb' : b0 < b → a0 * b0 < a * b := λ h, mul_lt_mul_of_le_of_lt ha h,
  exact ⟨(ha.eq_of_not_lt (λ h, absurd ab (ha' h).ne')).symm,
         (hb.eq_of_not_lt (λ h, absurd ab (hb' h).ne')).symm⟩,
end

[FR]

Maybe we need contrapositive lemmas of mul_lt_mul_of_lt_of_le and mul_lt_mul_of_le_of_lt

[FR]

@[to_additive] lemma eq_and_eq_of_le_of_le_of_mul_eq {A} [has_mul A] [linear_order A]
  [covariant_class A A (*) (≤)] [covariant_class A A (function.swap (*)) (<)]
  [contravariant_class A A (*) (≤)]
  {a b a0 b0 : A} (ha : a0 ≤ a) (hb : b0 ≤ b) (ab : a * b = a0 * b0) :
  a = a0 ∧ b = b0 :=
begin
  haveI := has_mul.to_covariant_class_right A,
  have ha' : ¬a0 * b0 < a * b → ¬a0 < a := mt (λ h, mul_lt_mul_of_lt_of_le h hb),
  have hb' : ¬a0 * b0 < a * b → ¬b0 < b := mt (λ h, mul_lt_mul_of_le_of_lt ha h),
  push_neg at ha' hb',
  exact ⟨ha.antisymm' (ha' ab.le), hb.antisymm' (hb' ab.le)⟩,
end

[Wrenna Robson]

Personally I'd split this lemma into two.

[Wrenna Robson]

The two halves seem to have little to do with one another.

[FR]

@[to_additive] lemma eq_and_eq_of_le_of_le_of_mul_eq {A} [has_mul A] [linear_order A]
  [covariant_class A A (*) (≤)] [covariant_class A A (function.swap (*)) (<)]
  [contravariant_class A A (*) (≤)]
  {a b a0 b0 : A} (ha : a0 ≤ a) (hb : b0 ≤ b) (ab : a * b = a0 * b0) :
  a = a0 ∧ b = b0 :=
begin
  haveI := has_mul.to_covariant_class_right A,
  haveI : contravariant_class A A (function.swap (*)) (≤) :=
    ⟨(covariant_lt_iff_contravariant_le A A (function.swap (*))).mp covariant_class.elim⟩,
  have ha' := λ h : a * b ≤ a0 * b0, le_of_mul_le_mul_right' (h.trans (mul_le_mul_left' hb _)),
  have hb' := λ h : a * b ≤ a0 * b0, le_of_mul_le_mul_left' (h.trans (mul_le_mul_right' ha _)),
  exact ⟨ha.antisymm' (ha' ab.le), hb.antisymm' (hb' ab.le)⟩,
end

The "direct" proof is longer, but I think it is possible to change the typeclass assumptions.

[Damiano Testa]

@FR thank you very much! I used one of your versions in the unique_prods PR!

[Damiano Testa]

@Wrenna Robson if this lemma were less specialized, I would probably split it. Since it is a technical step, I simply wanted to be done with it quickly.