α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ ∃ k, (∀ {x : α}, k < x → (x ∈ ∅ ↔ x ∈ A)) ∧ ¬k ∈ ∅ ∧ k ∈ A
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ toColex ∅ < toColex A
rw [Colex.lt_def]
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ ∀ {x : α}, max' A hA < x → (x ∈ ∅ ↔ x ∈ A)
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ ∃ k, (∀ {x : α}, k < x → (x ∈ ∅ ↔ x ∈ A)) ∧ ¬k ∈ ∅ ∧ k ∈ A
refine' ⟨max' _ hA, _, by simp, max'_mem _ _⟩
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ ∀ {x : α}, max' A hA < x → ¬x ∈ A
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ ∀ {x : α}, max' A hA < x → (x ∈ ∅ ↔ x ∈ A)
simp only [false_iff_iff, not_mem_empty]
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
x : α
hx : max' A hA < x
t : x ∈ A
⊢ False
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ ∀ {x : α}, max' A hA < x → ¬x ∈ A
intro x hx t
no goals
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
x : α
hx : max' A hA < x
t : x ∈ A
⊢ False
apply not_le_of_lt hx (le_max' _ _ t)
no goals
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ ¬max' A hA ∈ ∅
simp