α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₁ : ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
h₂ : ∀ (x : α), x ∈ B → x < t
⊢ ∀ (x : α), x ∈ A → x < t
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₁ : toColex A < toColex B
h₂ : ∀ (x : α), x ∈ B → x < t
⊢ ∀ (x : α), x ∈ A → x < t
rw [Colex.lt_def] at h₁
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
⊢ ∀ (x : α), x ∈ A → x < t
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₁ : ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
h₂ : ∀ (x : α), x ∈ B → x < t
⊢ ∀ (x : α), x ∈ A → x < t
rcases h₁ with ⟨k, z, _, _⟩
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
⊢ x < t
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
⊢ ∀ (x : α), x ∈ A → x < t
intro x hx
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
⊢ ¬x ≥ t
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
⊢ x < t
apply lt_of_not_ge
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
a : x ≥ t
⊢ False
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
⊢ ¬x ≥ t
intro a
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
a : x ≥ t
⊢ x ∈ B
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
a : x ≥ t
⊢ False
refine' not_lt_of_ge a (h₂ x _)
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
a : x ≥ t
⊢ k < x
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
a : x ≥ t
⊢ x ∈ B
rwa [← z]
no goals
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
a : x ≥ t
⊢ k < x
apply lt_of_lt_of_le (h₂ k ‹_›) a