-- Mathlib/Combinatorics/Colex.lean
lemma toColex_le_toColex_iff_max'_mem :
    toColex s ≤ toColex t ↔ ∀ hst : s ≠ t, (s ∆ t).max' (symmDiff_nonempty.2 hst) ∈ t

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : { ofColex := s } ≤ { ofColex := t }
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
hms : m ∈ s
⊢ False

Tactic:
have ⟨b, hbt, hbs, hmb⟩ := h hms hmt

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : { ofColex := s } ≤ { ofColex := t }
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
hms : m ∈ s
b : α
hbt : b ∈ { ofColex := t }.ofColex
hbs : b ∉ { ofColex := s }.ofColex
hmb : m ≤ b
⊢ False

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : { ofColex := s } ≤ { ofColex := t }
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
hms : m ∈ s
b : α
hbt : b ∈ { ofColex := t }.ofColex
hbs : b ∉ { ofColex := s }.ofColex
hmb : m ≤ b
⊢ False

Tactic:
exact lt_irrefl _ <| (max'_lt_iff _ _).1 (hmb.lt_of_ne <| ne_of_mem_of_not_mem hms hbs) _ <|
  mem_symmDiff.2 <| Or.inr ⟨hbt, hbs⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ { ofColex := s }.ofColex
hat : a ∉ { ofColex := t }.ofColex
hst : s ≠ t
⊢ ∃ b ∈ { ofColex := t }.ofColex, b ∉ { ofColex := s }.ofColex ∧ a ≤ b

Tactic:
refine ⟨_, h hst, ?_, le_max' _ _ <| mem_symmDiff.2 <| Or.inl ⟨has, hat⟩⟩

Result:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ { ofColex := s }.ofColex
hat : a ∉ { ofColex := t }.ofColex
hst : s ≠ t
⊢ (s ∆ t).max' ⋯ ∉ { ofColex := s }.ofColex

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : { ofColex := s } ≤ { ofColex := t }
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
⊢ m ∈ t

Tactic:
by_contra hmt

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : { ofColex := s } ≤ { ofColex := t }
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : { ofColex := s } ≤ { ofColex := t }
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
⊢ m ∈ s

Tactic:
simpa [m, mem_symmDiff, hmt] using max'_mem _ <| symmDiff_nonempty.2 hst

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ { ofColex := s }.ofColex
hat : a ∉ { ofColex := t }.ofColex
⊢ ∃ b ∈ { ofColex := t }.ofColex, b ∉ { ofColex := s }.ofColex ∧ a ≤ b

Tactic:
have hst : s ≠ t := ne_of_mem_of_not_mem' has hat

Result:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ { ofColex := s }.ofColex
hat : a ∉ { ofColex := t }.ofColex
hst : s ≠ t
⊢ ∃ b ∈ { ofColex := t }.ofColex, b ∉ { ofColex := s }.ofColex ∧ a ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ { ofColex := s } ≤ { ofColex := t } ↔ ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
refine ⟨fun h hst ↦ ?_, fun h a has hat ↦ ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : { ofColex := s } ≤ { ofColex := t }
hst : s ≠ t
⊢ (s ∆ t).max' ⋯ ∈ t

case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ { ofColex := s }.ofColex
hat : a ∉ { ofColex := t }.ofColex
⊢ ∃ b ∈ { ofColex := t }.ofColex, b ∉ { ofColex := s }.ofColex ∧ a ≤ b

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : { ofColex := s } ≤ { ofColex := t }
hst : s ≠ t
⊢ (s ∆ t).max' ⋯ ∈ t

Tactic:
set m := (s ∆ t).max' (symmDiff_nonempty.2 hst)

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : { ofColex := s } ≤ { ofColex := t }
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
⊢ m ∈ t

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ { ofColex := s }.ofColex
hat : a ∉ { ofColex := t }.ofColex
hst : s ≠ t
⊢ (s ∆ t).max' ⋯ ∉ { ofColex := s }.ofColex

Tactic:
simpa [mem_symmDiff, h hst] using max'_mem _ <| symmDiff_nonempty.2 hst

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : { ofColex := s } ≤ { ofColex := t }
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
⊢ False

Tactic:
have hms : m ∈ s := by
  simpa [m, mem_symmDiff, hmt] using max'_mem _ <| symmDiff_nonempty.2 hst

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : { ofColex := s } ≤ { ofColex := t }
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
hms : m ∈ s
⊢ False