-- Mathlib/Combinatorics/Colex.lean
lemma lt_iff_exists_filter_lt :
    toColex s < toColex t ↔ ∃ w ∈ t \ s, {a ∈ s | w < a} = {a ∈ t | w < a}

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Tactic:
refine ⟨m, hmt, hms, fun a hma ↦ ⟨fun has ↦ not_imp_comm.1 (hm _ has) hma.asymm, fun hat ↦ ?_⟩⟩

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
⊢ a ∈ s

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Tactic:
have hu : u.Nonempty := h.imp fun _ ↦ mem_u.2

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Tactic:
let m := max' _ hu

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
⊢ a ∈ s

Tactic:
by_contra has

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
has : a ∉ s
⊢ False

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
has : a ∉ s
⊢ False

Tactic:
have hau : a ∈ u := mem_u.2 ⟨hat, has, fun b hbs hbt ↦ (hm _ hbs hbt).trans hma⟩

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
has : a ∉ s
hau : a ∈ u
⊢ False

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
a : α
hma : m < a
hat : a ∈ t
has : a ∉ s
hau : a ∈ u
⊢ False

Tactic:
exact hma.not_le <| le_max' _ _ hau

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Tactic:
have ⟨hmt, hms, hm⟩ : m ∈ t ∧ m ∉ s ∧ ∀ a ∈ s, a ∉ t → a < m := mem_u.1 <| max'_mem _ _

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a) ↔ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)) → ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
w : α
⊢ w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w

Tactic:
simp [u, and_assoc]

Result:
no goals

Proof state:
case refine_2.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
a : α
has : a ∈ s
hat : a ∉ t
hwa : w ≤ a
⊢ False

Tactic:
exact hat <| (hw <| hwa.lt_of_ne <| ne_of_mem_of_not_mem hwt hat).1 has

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ { ofColex := s } < { ofColex := t } ↔ ∃ w ∈ t \ s, filter (fun a => w < a) s = filter (fun a => w < a) t

Tactic:
simp only [lt_iff_exists_forall_lt, mem_sdiff, filter_inj, and_assoc]

Result:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a) ↔ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Proof state:
case refine_2.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
a : α
has : a ∈ s
hat : a ∉ t
⊢ a < w

Tactic:
by_contra! hwa

Result:
case refine_2.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
a : α
has : a ∈ s
hat : a ∉ t
hwa : w ≤ a
⊢ False

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)) → ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Tactic:
rintro ⟨w, hwt, hws, hw⟩

Result:
case refine_2.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
⊢ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a