case nil
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? [] ix = get? l' (↑f ix)
⊢ [] <+ l'

case cons
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
⊢ hd :: tl <+ l'
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
⊢ l <+ l'
induction' l with hd tl IH generalizing l' f
case cons
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
this : some hd = get? l' (↑f 0)
⊢ hd :: tl <+ l'
case cons
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
⊢ hd :: tl <+ l'
have : some hd = _ := hf 0
case cons
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
this : ∃ h, get l' { val := ↑f 0, isLt := h } = hd
⊢ hd :: tl <+ l'
case cons
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
this : some hd = get? l' (↑f 0)
⊢ hd :: tl <+ l'
rw [eq_comm, List.get?_eq_some] at this
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
⊢ hd :: tl <+ l'
case cons
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
this : ∃ h, get l' { val := ↑f 0, isLt := h } = hd
⊢ hd :: tl <+ l'
obtain ⟨w, h⟩ := this
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
⊢ hd :: tl <+ l'
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
⊢ hd :: tl <+ l'
let f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) fun a b => by
    dsimp only
    rw [tsub_le_tsub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
    rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
    exact b.succ_pos
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ hd :: tl <+ l'
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
⊢ hd :: tl <+ l'
have : ∀ ix, tl.get? ix = (l'.drop (f 0 + 1)).get? (f' ix) := by
  intro ix
  rw [List.get?_drop, OrderEmbedding.coe_ofMapLEIff, add_tsub_cancel_of_le, ←hf, List.get?]
  rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
  exact ix.succ_pos
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ [hd] ++ tl <+ take (↑f 0 + 1) l' ++ drop (↑f 0 + 1) l'
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ hd :: tl <+ l'
rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ [hd] <+ take (↑f 0 + 1) l'
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ [hd] ++ tl <+ take (↑f 0 + 1) l' ++ drop (↑f 0 + 1) l'
apply List.Sublist.append _ (IH _ this)
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ get (take (Nat.succ (↑f 0)) l') { val := ↑f 0, isLt := (_ : ↑f 0 < length (take (Nat.succ (↑f 0)) l')) } ∈
    take (↑f 0 + 1) l'
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ [hd] <+ take (↑f 0 + 1) l'
rw [List.singleton_sublist, ← h, l'.get_take _ (Nat.lt_succ_self _)]
no goals
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ get (take (Nat.succ (↑f 0)) l') { val := ↑f 0, isLt := (_ : ↑f 0 < length (take (Nat.succ (↑f 0)) l')) } ∈
    take (↑f 0 + 1) l'
apply List.get_mem
no goals
case nil
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? [] ix = get? l' (↑f ix)
⊢ [] <+ l'
simp
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
a b : ℕ
⊢ ↑f (a + 1) - (↑f 0 + 1) ≤ ↑f (b + 1) - (↑f 0 + 1) ↔ a ≤ b
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
a b : ℕ
⊢ (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b
dsimp only
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
a b : ℕ
⊢ ↑f 0 + 1 ≤ ↑f (b + 1)
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
a b : ℕ
⊢ ↑f (a + 1) - (↑f 0 + 1) ≤ ↑f (b + 1) - (↑f 0 + 1) ↔ a ≤ b
rw [tsub_le_tsub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
a b : ℕ
⊢ 0 < b + 1
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
a b : ℕ
⊢ ↑f 0 + 1 ≤ ↑f (b + 1)
rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
no goals
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
a b : ℕ
⊢ 0 < b + 1
exact b.succ_pos
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
ix : ℕ
⊢ get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
⊢ ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
intro ix
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
ix : ℕ
⊢ ↑f 0 + 1 ≤ ↑f (ix + 1)
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
ix : ℕ
⊢ get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
rw [List.get?_drop, OrderEmbedding.coe_ofMapLEIff, add_tsub_cancel_of_le, ←hf, List.get?]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
ix : ℕ
⊢ 0 < ix + 1
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
ix : ℕ
⊢ ↑f 0 + 1 ≤ ↑f (ix + 1)
rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
no goals
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
ix : ℕ
⊢ 0 < ix + 1
exact ix.succ_pos