case intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k : ℕ
x : α
hx : x ∈ take k l
iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
⊢ r x (get (drop k l) { val := iy, isLt := hiy })
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k : ℕ
x y : α
hx : x ∈ take k l
hy : y ∈ drop k l
⊢ r x y
obtain ⟨⟨iy, hiy⟩, rfl⟩ := get_of_mem hy
case intro.mk.intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
ix : ℕ
hix : ix < length (take k l)
hx : get (take k l) { val := ix, isLt := hix } ∈ take k l
⊢ r (get (take k l) { val := ix, isLt := hix }) (get (drop k l) { val := iy, isLt := hiy })
case intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k : ℕ
x : α
hx : x ∈ take k l
iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
⊢ r x (get (drop k l) { val := iy, isLt := hiy })
obtain ⟨⟨ix, hix⟩, rfl⟩ := get_of_mem hx
case intro.mk.intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
ix : ℕ
hix : ix < length (take k l)
hx : get (take k l) { val := ix, isLt := hix } ∈ take k l
⊢ r (get l { val := ↑{ val := ix, isLt := hix }, isLt := (_ : ↑{ val := ix, isLt := hix } < length l) })
    (get l { val := k + ↑{ val := iy, isLt := hiy }, isLt := (_ : k + ↑{ val := iy, isLt := hiy } < length l) })
case intro.mk.intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
ix : ℕ
hix : ix < length (take k l)
hx : get (take k l) { val := ix, isLt := hix } ∈ take k l
⊢ r (get (take k l) { val := ix, isLt := hix }) (get (drop k l) { val := iy, isLt := hiy })
rw [get_take', get_drop']
case intro.mk.intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
ix : ℕ
hix✝ : ix < length (take k l)
hix : ix < min k (length l)
hx : get (take k l) { val := ix, isLt := hix✝ } ∈ take k l
⊢ r (get l { val := ↑{ val := ix, isLt := hix✝ }, isLt := (_ : ↑{ val := ix, isLt := hix✝ } < length l) })
    (get l { val := k + ↑{ val := iy, isLt := hiy }, isLt := (_ : k + ↑{ val := iy, isLt := hiy } < length l) })
case intro.mk.intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
ix : ℕ
hix : ix < length (take k l)
hx : get (take k l) { val := ix, isLt := hix } ∈ take k l
⊢ r (get l { val := ↑{ val := ix, isLt := hix }, isLt := (_ : ↑{ val := ix, isLt := hix } < length l) })
    (get l { val := k + ↑{ val := iy, isLt := hiy }, isLt := (_ : k + ↑{ val := iy, isLt := hiy } < length l) })
rw [length_take] at hix
no goals
case intro.mk.intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
ix : ℕ
hix✝ : ix < length (take k l)
hix : ix < min k (length l)
hx : get (take k l) { val := ix, isLt := hix✝ } ∈ take k l
⊢ r (get l { val := ↑{ val := ix, isLt := hix✝ }, isLt := (_ : ↑{ val := ix, isLt := hix✝ } < length l) })
    (get l { val := k + ↑{ val := iy, isLt := hiy }, isLt := (_ : k + ↑{ val := iy, isLt := hiy } < length l) })
exact h.rel_nthLe_of_lt _ _ (ix.lt_add_right _ _ (lt_min_iff.mp hix).left)