α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s ↔ ∀ (x : α), x ∈ s → x < r
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ toColex s < toColex {r} ↔ ∀ (x : α), x ∈ s → x < r
simp only [lt_def, mem_singleton, ← and_assoc, exists_eq_right]
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s → ∀ (x : α), x ∈ s → x < r

case mpr
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ (∀ (x : α), x ∈ s → x < r) → (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s ↔ ∀ (x : α), x ∈ s → x < r
constructor
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
⊢ x < r
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s → ∀ (x : α), x ∈ s → x < r
intro t x hx
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
⊢ ¬r ≤ x
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
⊢ x < r
rw [← not_le]
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
h : r ≤ x
⊢ False
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
⊢ ¬r ≤ x
intro h
case mp.inl
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
h : r ≤ x
h₁ : r < x
⊢ False

case mp.inr
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
hx : r ∈ s
h : r ≤ r
⊢ False
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
h : r ≤ x
⊢ False
rcases lt_or_eq_of_le h with (h₁ | rfl)
no goals
case mp.inl
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
h : r ≤ x
h₁ : r < x
⊢ False
exact ne_of_irrefl h₁ ((t.1 h₁).1 hx).symm
no goals
case mp.inr
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
hx : r ∈ s
h : r ≤ r
⊢ False
exact t.2 hx
no goals
case mpr
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ (∀ (x : α), x ∈ s → x < r) → (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
exact fun h =>
  ⟨@fun z hz => ⟨@fun i => (asymm hz (h _ i)).elim, @fun i => (hz.ne' i).elim⟩,
      by simpa using h r⟩
no goals
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
h : ∀ (x : α), x ∈ s → x < r
⊢ ¬r ∈ s
simpa using h r