golfing `Ico` union, take 2

Stream: new members

[Snir Broshi]

Hey, I was just watching a livestream by Kevin from 2020 about the thread #maths > golfing `Ico` union

which contains multiple long-ish proofs of this statement:

import Mathlib
open Set
example {α} [LinearOrder α] (a b c : α) :
    Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c := by
  sorry

[Snir Broshi]

For example this is Kenny's proof translated to modern-day mathlib:

import Mathlib
open Set
example {α} [LinearOrder α] (a b c : α) : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c := by
  rcases le_total a b with hab | hba <;> rcases le_total b c with hbc | hcb
  · rw [Ico_eq_empty_of_le hab, Ico_eq_empty_of_le hbc, Ico_eq_empty_of_le (le_trans hab hbc),
      empty_union, empty_union, union_empty, Ico_union_Ico_eq_Ico hab hbc]
  · rcases le_total a c with hac | hca
    · rw [Ico_eq_empty_of_le hac, Ico_eq_empty_of_le hcb, Ico_eq_empty_of_le hab,
        empty_union, union_empty, union_empty, union_comm, Ico_union_Ico_eq_Ico hac hcb]
    · rw [Ico_eq_empty_of_le hca, Ico_eq_empty_of_le hcb, Ico_eq_empty_of_le hab,
        empty_union, union_empty, union_empty, union_comm, Ico_union_Ico_eq_Ico hca hab]
  · rcases le_total a c with hac | hca
    · rw [Ico_eq_empty_of_le hac, Ico_eq_empty_of_le hbc, Ico_eq_empty_of_le hba,
        empty_union, union_empty, union_empty, Ico_union_Ico_eq_Ico hba hac]
    · rw [Ico_eq_empty_of_le hca, Ico_eq_empty_of_le hbc, Ico_eq_empty_of_le hba,
        empty_union, union_empty, union_empty, Ico_union_Ico_eq_Ico hbc hca]
  · rw [Ico_eq_empty_of_le hcb, Ico_eq_empty_of_le hba, Ico_eq_empty_of_le (le_trans hcb hba),
      empty_union, empty_union, union_empty, union_comm, Ico_union_Ico_eq_Ico hcb hba]

[Snir Broshi]

The point of that thread is that it's a simple fact with an annoying proof that should be solvable by automation, but isn't

[Snir Broshi]

Well now:

import Mathlib
open Set

example {α} [LinearOrder α] (a b c : α) : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c := by
  grind

:tada:
(I just thought that was incredible progress by Lean and wanted to share)