/-
Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury G. Kudryashov

! This file was ported from Lean 3 source module data.list.nodup_equiv_fin
! leanprover-community/mathlib commit 008205aa645b3f194c1da47025c5f110c8406eab
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fin.Basic
import Mathlib.Data.List.Sort
import Mathlib.Data.List.Duplicate

/-!
# Equivalence between `Fin (length l)` and elements of a list

Given a list `l`,

* if `l` has no duplicates, then `List.Nodup.getEquiv` is the equivalence between
  `Fin (length l)` and `{x // x ∈ l}` sending `i` to `⟨get l i, _⟩` with the inverse
  sending `⟨x, hx⟩` to `⟨indexOf x l, _⟩`;

* if `l` has no duplicates and contains every element of a type `α`, then
  `List.Nodup.getEquivOfForallMemList` defines an equivalence between
  `Fin (length l)` and `α`;  if `α` does not have decidable equality, then
  there is a bijection `List.Nodup.getBijectionOfForallMemList`;

* if `l` is sorted w.r.t. `(<)`, then `List.Sorted.getIso` is the same bijection reinterpreted
  as an `OrderIso`.

-/


namespace List

variable {
α: Type ?u.2
α : 
Type _: Type (?u.2+1)
Type _}

namespace Nodup

/-- If `l` lists all the elements of `α` without duplicates, then `List.get` defines
a bijection `Fin l.length → α`.  See `List.Nodup.getEquivOfForallMemList`
for a version giving an equivalence when there is decidable equality. -/
@[
simps: ∀ {α : Type u_1} (l : List α) (nd : Nodup l) (h : ∀ (x : α), x ∈ l) (i : Fin (length l)),
  ↑(getBijectionOfForallMemList l nd h) i = get l i
simps]
def 
getBijectionOfForallMemList: {α : Type u_1} → (l : List α) → Nodup l → (∀ (x : α), x ∈ l) → { f // Function.Bijective f }
getBijectionOfForallMemList (
l: List α
l : 
List: Type ?u.8 → Type ?u.8
List 
α: Type ?u.5
α) (
nd: Nodup l
nd : 
l: List α
l.
Nodup: {α : Type ?u.11} → List α → Prop
Nodup) (
h: ∀ (x : α), x ∈ l
h : ∀ 
x: α
x : 
α: Type ?u.5
α, 
x: α
x ∈ 
l: List α
l) :
    { 
f: Fin (length l) → α
f : 
Fin: ℕ → Type
Fin 
l: List α
l.
length: {α : Type ?u.52} → List α → ℕ
length → 
α: Type ?u.5
α // 
Function.Bijective: {α : Sort ?u.60} → {β : Sort ?u.59} → (α → β) → Prop
Function.Bijective 
f: Fin (length l) → α
f } :=
  ⟨fun 
i: ?m.89
i => 
l: List α
l.
get: {α : Type ?u.91} → (as : List α) → Fin (length as) → α
get 
i: ?m.89
i, fun 
_: ?m.106
_ 
_: ?m.109
_ 
h: ?m.112
h => 
Fin.ext: ∀ {n : ℕ} {a b : Fin n}, ↑a = ↑b → a = b
Fin.ext <| (
nd: Nodup l
nd.
nthLe_inj_iff: ∀ {α : Type ?u.120} {l : List α},
  Nodup l → ∀ {i j : ℕ} (hi : i < length l) (hj : j < length l), nthLe l i hi = nthLe l j hj ↔ i = j
nthLe_inj_iff 
_: ?m.132 < length ?m.129
_ 
_: ?m.133 < length ?m.129
_).
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 
h: ?m.112
h,
   fun 
x: ?m.184
x =>
    let ⟨
i: Fin (length l)
i, 
hl: get l i = x
hl⟩ := 
List.mem_iff_get: ∀ {α : Type ?u.186} {a : α} {l : List α}, a ∈ l ↔ ∃ n, get l n = a
List.mem_iff_get.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 (
h: ∀ (x : α), x ∈ l
h 
x: ?m.184
x)
    ⟨
i: Fin (length l)
i, 
hl: get l i = x
hl⟩⟩
#align list.nodup.nth_le_bijection_of_forall_mem_list 
List.Nodup.getBijectionOfForallMemList: {α : Type u_1} → (l : List α) → Nodup l → (∀ (x : α), x ∈ l) → { f // Function.Bijective f }
List.Nodup.getBijectionOfForallMemList

variable [
DecidableEq: Sort ?u.465 → Sort (max1?u.465)
DecidableEq 
α: Type ?u.474
α]

/-- If `l` has no duplicates, then `List.get` defines an equivalence between `Fin (length l)` and
the set of elements of `l`. -/
@[
simps: ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (H : Nodup l) (i : Fin (length l)), ↑(↑(getEquiv l H) i) = get l i
simps]
def 
getEquiv: {α : Type u_1} → [inst : DecidableEq α] → (l : List α) → Nodup l → Fin (length l) ≃ { x // x ∈ l }
getEquiv (
l: List α
l : 
List: Type ?u.486 → Type ?u.486
List 
α: Type ?u.474
α) (
H: Nodup l
H : 
Nodup: {α : Type ?u.489} → List α → Prop
Nodup 
l: List α
l) : 
Fin: ℕ → Type
Fin (
length: {α : Type ?u.497} → List α → ℕ
length 
l: List α
l) ≃ { 
x: ?m.503
x // 
x: ?m.503
x ∈ 
l: List α
l } where
  toFun 
i: ?m.533
i := ⟨
get: {α : Type ?u.547} → (as : List α) → Fin (length as) → α
get 
l: List α
l 
i: ?m.533
i, 
get_mem: ∀ {α : Type ?u.550} (l : List α) (n : ℕ) (h : n < length l), get l { val := n, isLt := h } ∈ l
get_mem 
l: List α
l 
i: ?m.533
i 
i: ?m.533
i.
2: ∀ {n : ℕ} (self : Fin n), ↑self < n
2⟩
  invFun 
x: ?m.667
x := ⟨
indexOf: {α : Type ?u.673} → [inst : BEq α] → α → List α → ℕ
indexOf (↑
x: ?m.667
x) 
l: List α
l, 
indexOf_lt_length: ∀ {α : Type ?u.735} [inst : DecidableEq α] {a : α} {l : List α}, indexOf a l < length l ↔ a ∈ l
indexOf_lt_length.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
x: ?m.667
x.
2: ∀ {α : Sort ?u.811} {p : α → Prop} (self : Subtype p), p ↑self
2⟩
  left_inv 
i: ?m.851
i := by
Goals accomplished! 🐙 
α: Type ?u.474

inst✝: DecidableEq α

l: List α

H: Nodup l

i: Fin (length l)

(fun x => { val := indexOf (↑x) l, isLt := (_ : indexOf (↑x) l < length l) })
    ((fun i => { val := get l i, property := (_ : get l { val := ↑i, isLt := (_ : ↑i < length l) } ∈ l) }) i) =   isimp only [
List.get_indexOf: ∀ {α : Type ?u.1039} [inst : DecidableEq α] {l : List α}, Nodup l → ∀ (i : Fin (length l)), indexOf (get l i) l = ↑i
List.get_indexOf, 
eq_self_iff_true: ∀ {α : Sort ?u.1060} (a : α), a = a ↔ True
eq_self_iff_true, 
Fin.eta: ∀ {n : ℕ} (a : Fin n) (h : ↑a < n), { val := ↑a, isLt := h } = a
Fin.eta, 
Subtype.coe_mk: ∀ {α : Sort ?u.1083} {p : α → Prop} (a : α) (h : p a), ↑{ val := a, property := h } = a
Subtype.coe_mk, 
H: Nodup l
H]
Goals accomplished! 🐙
  right_inv 
x: ?m.857
x := by
Goals accomplished! 🐙 
α: Type ?u.474

inst✝: DecidableEq α

l: List α

H: Nodup l

x: { x // x ∈ l }

(fun i => { val := get l i, property := (_ : get l { val := ↑i, isLt := (_ : ↑i < length l) } ∈ l) })
    ((fun x => { val := indexOf (↑x) l, isLt := (_ : indexOf (↑x) l < length l) }) x) =   xsimp
Goals accomplished! 🐙
#align list.nodup.nth_le_equiv 
List.Nodup.getEquiv: {α : Type u_1} → [inst : DecidableEq α] → (l : List α) → Nodup l → Fin (length l) ≃ { x // x ∈ l }
List.Nodup.getEquiv

/-- If `l` lists all the elements of `α` without duplicates, then `List.get` defines
an equivalence between `Fin l.length` and `α`.

See `List.Nodup.getBijectionOfForallMemList` for a version without
decidable equality. -/
@[
simps: ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (nd : Nodup l) (h : ∀ (x : α), x ∈ l) (a : α),
  ↑(↑(getEquivOfForallMemList l nd h).symm a) = indexOf a l
simps]
def 
getEquivOfForallMemList: (l : List α) → Nodup l → (∀ (x : α), x ∈ l) → Fin (length l) ≃ α
getEquivOfForallMemList (
l: List α
l : 
List: Type ?u.2782 → Type ?u.2782
List 
α: Type ?u.2770
α) (
nd: Nodup l
nd : 
l: List α
l.
Nodup: {α : Type ?u.2785} → List α → Prop
Nodup) (
h: ∀ (x : α), x ∈ l
h : ∀ 
x: α
x : 
α: Type ?u.2770
α, 
x: α
x ∈ 
l: List α
l) : 
Fin: ℕ → Type
Fin 
l: List α
l.
length: {α : Type ?u.2824} → List α → ℕ
length ≃ 
α: Type ?u.2770
α
    where
  toFun 
i: ?m.2840
i := 
l: List α
l.
get: {α : Type ?u.2842} → (as : List α) → Fin (length as) → α
get 
i: ?m.2840
i
  invFun 
a: ?m.2851
a := ⟨
_: ℕ
_, 
indexOf_lt_length: ∀ {α : Type ?u.2858} [inst : DecidableEq α] {a : α} {l : List α}, indexOf a l < length l ↔ a ∈ l
indexOf_lt_length.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (
h: ∀ (x : α), x ∈ l
h 
a: ?m.2851
a)⟩
  left_inv 
i: ?m.2928
i := by
Goals accomplished! 🐙 
α: Type ?u.2770

inst✝: DecidableEq α

l: List α

nd: Nodup l

h: ∀ (x : α), x ∈ l

i: Fin (length l)

(fun a => { val := indexOf a l, isLt := (_ : indexOf a l < length l) }) ((fun i => get l i) i) = isimp [
List.get_indexOf: ∀ {α : Type ?u.2980} [inst : DecidableEq α] {l : List α}, Nodup l → ∀ (i : Fin (length l)), indexOf (get l i) l = ↑i
List.get_indexOf, 
nd: Nodup l
nd]
Goals accomplished! 🐙
  right_inv 
a: ?m.2934
a := by
Goals accomplished! 🐙 
α: Type ?u.2770

inst✝: DecidableEq α

l: List α

nd: Nodup l

h: ∀ (x : α), x ∈ l

a: α

(fun i => get l i) ((fun a => { val := indexOf a l, isLt := (_ : indexOf a l < length l) }) a) = asimp
Goals accomplished! 🐙
#align list.nodup.nth_le_equiv_of_forall_mem_list 
List.Nodup.getEquivOfForallMemList: {α : Type u_1} → [inst : DecidableEq α] → (l : List α) → Nodup l → (∀ (x : α), x ∈ l) → Fin (length l) ≃ α
List.Nodup.getEquivOfForallMemList

end Nodup

namespace Sorted

variable [
Preorder: Type ?u.6846 → Type ?u.6846
Preorder 
α: Type ?u.5749
α] {
l: List α
l : 
List: Type ?u.6013 → Type ?u.6013
List 
α: Type ?u.5740
α}

theorem 
get_mono: Sorted (fun x x_1 => x ≤ x_1) l → Monotone (get l)
get_mono (
h: Sorted (fun x x_1 => x ≤ x_1) l
h : 
l: List α
l.
Sorted: {α : Type ?u.5758} → (α → α → Prop) → List α → Prop
Sorted 
(· ≤ ·): α → α → Prop
(· ≤ ·)) : 
Monotone: {α : Type ?u.5831} → {β : Type ?u.5830} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone 
l: List α
l.
get: {α : Type ?u.5872} → (as : List α) → Fin (length as) → α
get := fun 
_: ?m.5925
_ 
_: ?m.5928
_ => 
h: Sorted (fun x x_1 => x ≤ x_1) l
h.
rel_get_of_le: ∀ {α : Type ?u.5930} {r : α → α → Prop} [inst : IsRefl α r] {l : List α},
  Sorted r l → ∀ {a b : Fin (length l)}, a ≤ b → r (get l a) (get l b)
rel_get_of_le
#align list.sorted.nth_le_mono 
List.Sorted.get_mono: ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, Sorted (fun x x_1 => x ≤ x_1) l → Monotone (get l)
List.Sorted.get_mono

theorem 
get_strictMono: Sorted (fun x x_1 => x < x_1) l → StrictMono (get l)
get_strictMono (
h: Sorted (fun x x_1 => x < x_1) l
h : 
l: List α
l.
Sorted: {α : Type ?u.6016} → (α → α → Prop) → List α → Prop
Sorted 
(· < ·): α → α → Prop
(· < ·)) : 
StrictMono: {α : Type ?u.6086} → {β : Type ?u.6085} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
StrictMono 
l: List α
l.
get: {α : Type ?u.6127} → (as : List α) → Fin (length as) → α
get := fun 
_: ?m.6180
_ 
_: ?m.6183
_ => 
h: Sorted (fun x x_1 => x < x_1) l
h.
rel_get_of_lt: ∀ {α : Type ?u.6185} {r : α → α → Prop} {l : List α},
  Sorted r l → ∀ {a b : Fin (length l)}, a < b → r (get l a) (get l b)
rel_get_of_lt
#align list.sorted.nth_le_strict_mono 
List.Sorted.get_strictMono: ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, Sorted (fun x x_1 => x < x_1) l → StrictMono (get l)
List.Sorted.get_strictMono

variable [
DecidableEq: Sort ?u.6244 → Sort (max1?u.6244)
DecidableEq 
α: Type ?u.6843
α]

/-- If `l` is a list sorted w.r.t. `(<)`, then `List.get` defines an order isomorphism between
`Fin (length l)` and the set of elements of `l`. -/
def 
getIso: {α : Type u_1} →
  [inst : Preorder α] →
    [inst_1 : DecidableEq α] → (l : List α) → Sorted (fun x x_1 => x < x_1) l → Fin (length l) ≃o { x // x ∈ l }
getIso (
l: List α
l : 
List: Type ?u.6271 → Type ?u.6271
List 
α: Type ?u.6253
α) (
H: Sorted (fun x x_1 => x < x_1) l
H : 
Sorted: {α : Type ?u.6274} → (α → α → Prop) → List α → Prop
Sorted 
(· < ·): α → α → Prop
(· < ·) 
l: List α
l) : 
Fin: ℕ → Type
Fin (
length: {α : Type ?u.6343} → List α → ℕ
length 
l: List α
l) ≃o { 
x: ?m.6349
x // 
x: ?m.6349
x ∈ 
l: List α
l } where
  toEquiv := 
H: Sorted (fun x x_1 => x < x_1) l
H.
nodup: ∀ {α : Type ?u.6438} {r : α → α → Prop} [inst : IsIrrefl α r] {l : List α}, Sorted r l → Nodup l
nodup.
getEquiv: {α : Type ?u.6476} → [inst : DecidableEq α] → (l : List α) → Nodup l → Fin (length l) ≃ { x // x ∈ l }
getEquiv 
l: List α
l
  map_rel_iff' := 
H: Sorted (fun x x_1 => x < x_1) l
H.
get_strictMono: ∀ {α : Type ?u.6530} [inst : Preorder α] {l : List α}, Sorted (fun x x_1 => x < x_1) l → StrictMono (get l)
get_strictMono.
le_iff_le: ∀ {α : Type ?u.6541} {β : Type ?u.6540} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
le_iff_le
#align list.sorted.nth_le_iso 
List.Sorted.getIso: {α : Type u_1} →
  [inst : Preorder α] →
    [inst_1 : DecidableEq α] → (l : List α) → Sorted (fun x x_1 => x < x_1) l → Fin (length l) ≃o { x // x ∈ l }
List.Sorted.getIso

variable (
H: Sorted (fun x x_1 => x < x_1) l
H : 
Sorted: {α : Type ?u.6977} → (α → α → Prop) → List α → Prop
Sorted 
(· < ·): α → α → Prop
(· < ·) 
l: List α
l) {
x: { x // x ∈ l }
x : { 
x: ?m.7047
x // 
x: ?m.6931
x ∈ 
l: List α
l }} {
i: Fin (length l)
i : 
Fin: ℕ → Type
Fin 
l: List α
l.
length: {α : Type ?u.7069} → List α → ℕ
length}

@[simp]
theorem 
coe_getIso_apply: ∀ {α : Type u_1} [inst : Preorder α] {l : List α} [inst_1 : DecidableEq α] (H : Sorted (fun x x_1 => x < x_1) l)
  {i : Fin (length l)}, ↑(↑(getIso l H) i) = get l i
coe_getIso_apply : (
H: Sorted (fun x x_1 => x < x_1) l
H.
getIso: {α : Type ?u.7091} →
  [inst : Preorder α] →
    [inst_1 : DecidableEq α] → (l : List α) → Sorted (fun x x_1 => x < x_1) l → Fin (length l) ≃o { x // x ∈ l }
getIso 
l: List α
l 
i: Fin (length l)
i : 
α: Type ?u.6959
α) = 
get: {α : Type ?u.7389} → (as : List α) → Fin (length as) → α
get 
l: List α
l 
i: Fin (length l)
i :=
  
rfl: ∀ {α : Sort ?u.7394} {a : α}, a = a
rfl
#align list.sorted.coe_nth_le_iso_apply 
List.Sorted.coe_getIso_apply: ∀ {α : Type u_1} [inst : Preorder α] {l : List α} [inst_1 : DecidableEq α] (H : Sorted (fun x x_1 => x < x_1) l)
  {i : Fin (length l)}, ↑(↑(getIso l H) i) = get l i
List.Sorted.coe_getIso_apply

@[simp]
theorem 
coe_getIso_symm_apply: ∀ {α : Type u_1} [inst : Preorder α] {l : List α} [inst_1 : DecidableEq α] (H : Sorted (fun x x_1 => x < x_1) l)
  {x : { x // x ∈ l }}, ↑(↑(OrderIso.symm (getIso l H)) x) = indexOf (↑x) l
coe_getIso_symm_apply : ((
H: Sorted (fun x x_1 => x < x_1) l
H.
getIso: {α : Type ?u.7612} →
  [inst : Preorder α] →
    [inst_1 : DecidableEq α] → (l : List α) → Sorted (fun x x_1 => x < x_1) l → Fin (length l) ≃o { x // x ∈ l }
getIso 
l: List α
l).
symm: {α : Type ?u.7679} → {β : Type ?u.7678} → [inst : LE α] → [inst_1 : LE β] → α ≃o β → β ≃o α
symm 
x: { x // x ∈ l }
x : 
ℕ: Type
ℕ) = 
indexOf: {α : Type ?u.7931} → [inst : BEq α] → α → List α → ℕ
indexOf (↑
x: { x // x ∈ l }
x) 
l: List α
l :=
  
rfl: ∀ {α : Sort ?u.8090} {a : α}, a = a
rfl
#align list.sorted.coe_nth_le_iso_symm_apply 
List.Sorted.coe_getIso_symm_apply: ∀ {α : Type u_1} [inst : Preorder α] {l : List α} [inst_1 : DecidableEq α] (H : Sorted (fun x x_1 => x < x_1) l)
  {x : { x // x ∈ l }}, ↑(↑(OrderIso.symm (getIso l H)) x) = indexOf (↑x) l
List.Sorted.coe_getIso_symm_apply

end Sorted

section Sublist

/-- If there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`,
then `Sublist l l'`.
-/
theorem 
sublist_of_orderEmbedding_get?_eq: ∀ {l l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) → l <+ l'
sublist_of_orderEmbedding_get?_eq {
l: List α
l 
l': List α
l' : 
List: Type ?u.8220 → Type ?u.8220
List 
α: Type ?u.8214
α} (
f: ℕ ↪o ℕ
f : 
ℕ: Type
ℕ ↪o 
ℕ: Type
ℕ)
    (
hf: ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
hf : ∀ 
ix: ℕ
ix : 
ℕ: Type
ℕ, 
l: List α
l.
get?: {α : Type ?u.8236} → List α → ℕ → Option α
get? 
ix: ℕ
ix = 
l': List α
l'.
get?: {α : Type ?u.8242} → List α → ℕ → Option α
get? (
f: ℕ ↪o ℕ
f 
ix: ℕ
ix)) : 
l: List α
l <+ 
l': List α
l' := by
Goals accomplished! 🐙
  
α: Type u_1

l, l': List α

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)

l <+ l'induction' 
l: List α
l with 
hd: ?m.8440
hd 
tl: List ?m.8440
tl 
IH: ?m.8441 tl
IH generalizing 
l': List α
l' 
f: ℕ ↪o ℕ
f
α: 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)

nil
[] <+ 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)

cons
hd :: tl <+ l'
  
α: Type u_1

l, l': List α

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)

l <+ l'·
α: 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)

nil
[] <+ l' 
α: 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)

nil
[] <+ 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)

cons
hd :: tl <+ l'simp
Goals accomplished! 🐙
  
α: Type u_1

l, l': List α

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)

l <+ l'have : 
some: {α : Type ?u.8496} → α → Option α
some 
hd: ?m.8440
hd = 
_: ?m.8499
_ := 
hf: ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
hf 
0: ?m.8503
0
α: 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)

cons
hd :: tl <+ l'
  
α: Type u_1

l, l': List α

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)

l <+ l'rw [
α: 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)

cons
hd :: tl <+ l'
eq_comm: ∀ {α : Sort ?u.8533} {a b : α}, a = b ↔ b = a
eq_comm,
α: 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: get? l' (↑f 0) = some hd

cons
hd :: tl <+ 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)

this: some hd = get? l' (↑f 0)

cons
hd :: tl <+ l'
List.get?_eq_some: ∀ {α : Type ?u.8566} {a : α} {l : List α} {n : ℕ}, get? l n = some a ↔ ∃ h, get l { val := n, isLt := h } = a
List.get?_eq_some
α: 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

cons
hd :: tl <+ 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)

this: ∃ h, get l' { val := ↑f 0, isLt := h } = hd

cons
hd :: tl <+ l' at 
this: some hd = ?m.8500
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)

this: ∃ h, get l' { val := ↑f 0, isLt := h } = hd

cons
hd :: tl <+ l'
  
α: Type u_1

l, l': List α

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)

l <+ l'obtain 
⟨w, h⟩: ∃ h, get l' { val := ↑f 0, isLt := h } = hd
⟨
w: ↑f 0 < length l'
w
⟨w, h⟩: ∃ h, get l' { val := ↑f 0, isLt := h } = hd
, 
h: get l' { val := ↑f 0, isLt := w } = hd
h
⟨w, h⟩: ∃ h, get l' { val := ↑f 0, isLt := h } = hd
⟩ := 
this: ∃ h, get l' { val := ↑f 0, isLt := h } = hd
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

cons.intro
hd :: tl <+ l'
  
α: Type u_1

l, l': List α

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)

l <+ l'let 
f': ℕ ↪o ℕ
f' : 
ℕ: Type
ℕ ↪o 
ℕ: Type
ℕ :=
    
OrderEmbedding.ofMapLEIff: {α : Type ?u.8642} →
  {β : Type ?u.8641} →
    [inst : PartialOrder α] → [inst_1 : Preorder β] → (f : α → β) → (∀ (a b : α), f a ≤ f b ↔ a ≤ b) → α ↪o β
OrderEmbedding.ofMapLEIff (fun 
i: ?m.8786
i => 
f: ℕ ↪o ℕ
f (
i: ?m.8786
i + 
1: ?m.8914
1) - (
f: ℕ ↪o ℕ
f 
0: ?m.9093
0 + 
1: ?m.9096
1)) fun 
a: ?m.9179
a 
b: ?m.9182
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

cons.intro
hd :: tl <+ l'by
Goals accomplished! 🐙
      
α: 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 ≤ bdsimp 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 (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 ≤ brw [
α: 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
tsub_le_tsub_iff_right: ∀ {α : Type ?u.9233} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
  [inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst : OrderedSub α]
  {a b c : α}, c ≤ b → (a - c ≤ b - c ↔ a ≤ b)
tsub_le_tsub_iff_right,
α: 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 (b + 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: ℕ

↑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
OrderEmbedding.le_iff_le: ∀ {α : Type ?u.9629} {β : Type ?u.9628} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) {a b : α},
  ↑f a ≤ ↑f b ↔ a ≤ b
OrderEmbedding.le_iff_le,
α: 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: ℕ

a + 1 ≤ b + 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: ℕ

↑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
Nat.succ_le_succ_iff: ∀ {a b : ℕ}, Nat.succ a ≤ Nat.succ b ↔ a ≤ b
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: ℕ

a ≤ b ↔ 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: ℕ

↑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 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: ℕ

(fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ brw [
α: 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)
Nat.succ_le_iff: ∀ {m n : ℕ}, Nat.succ m ≤ n ↔ m < n
Nat.succ_le_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: ℕ

↑f 0 < ↑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 0 + 1 ≤ ↑f (b + 1)
OrderEmbedding.lt_iff_lt: ∀ {α : Type ?u.9804} {β : Type ?u.9803} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) {a b : α},
  ↑f a < ↑f b ↔ a < b
OrderEmbedding.lt_iff_lt
α: 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: ℕ

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: ℕ

(fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ bexact 
b: ℕ
b.
succ_pos: ∀ (n : ℕ), 0 < Nat.succ n
succ_pos
Goals accomplished! 🐙
  
α: Type u_1

l, l': List α

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)

l <+ l'have : ∀ 
ix: ?m.9951
ix, 
tl: List ?m.8440
tl.
get?: {α : Type ?u.9955} → List α → ℕ → Option α
get? 
ix: ?m.9951
ix = (
l': List α
l'.
drop: {α : Type ?u.9960} → ℕ → List α → List α
drop (
f: ℕ ↪o ℕ
f 
0: ?m.10088
0 + 
1: ?m.10091
1)).
get?: {α : Type ?u.10128} → List α → ℕ → Option α
get? (
f': ℕ ↪o ℕ
f' 
ix: ?m.9951
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':= 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): ℕ ↪o ℕ

cons.intro
hd :: tl <+ l'by
Goals accomplished! 🐙
    
α: 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':= 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): ℕ ↪o ℕ

∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)intro 
ix: ℕ
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':= 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): ℕ ↪o ℕ

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':= 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): ℕ ↪o ℕ

∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)rw [
α: 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':= 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): ℕ ↪o ℕ

ix: ℕ

get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
List.get?_drop: ∀ {α : Type ?u.10260} (L : List α) (i j : ℕ), get? (drop i L) j = get? L (i + j)
List.get?_drop,
α: 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':= 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): ℕ ↪o ℕ

ix: ℕ

get? tl ix = get? l' (↑f 0 + 1 + ↑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':= 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): ℕ ↪o ℕ

ix: ℕ

get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
OrderEmbedding.coe_ofMapLEIff: ∀ {α : Type ?u.10285} {β : Type ?u.10286} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β}
  (h : ∀ (a b : α), f a ≤ f b ↔ a ≤ b), ↑(OrderEmbedding.ofMapLEIff f h) = f
OrderEmbedding.coe_ofMapLEIff,
α: 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':= 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): ℕ ↪o ℕ

ix: ℕ

get? tl ix = get? l' (↑f 0 + 1 + (↑f (ix + 1) - (↑f 0 + 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':= 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): ℕ ↪o ℕ

ix: ℕ

get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
add_tsub_cancel_of_le: ∀ {α : Type ?u.10477} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
  [inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
  {a b : α}, a ≤ b → a + (b - a) = b
add_tsub_cancel_of_le,
α: 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':= 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): ℕ ↪o ℕ

ix: ℕ

get? tl ix = get? l' (↑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':= 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): ℕ ↪o ℕ

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':= 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): ℕ ↪o ℕ

ix: ℕ

get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)←
hf: ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
hf,
α: 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':= 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): ℕ ↪o ℕ

ix: ℕ

get? tl ix = get? (hd :: tl) (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':= 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): ℕ ↪o ℕ

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':= 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): ℕ ↪o ℕ

ix: ℕ

get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
List.get?: {α : Type ?u.15601} → List α → ℕ → Option α
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':= 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): ℕ ↪o ℕ

ix: ℕ

get? tl ix = get? tl 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':= 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): ℕ ↪o ℕ

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':= 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): ℕ ↪o ℕ

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':= 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): ℕ ↪o ℕ

∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)rw [
α: 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':= 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): ℕ ↪o ℕ

ix: ℕ

↑f 0 + 1 ≤ ↑f (ix + 1)
Nat.succ_le_iff: ∀ {m n : ℕ}, Nat.succ m ≤ n ↔ m < n
Nat.succ_le_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

f':= 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): ℕ ↪o ℕ

ix: ℕ

↑f 0 < ↑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':= 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): ℕ ↪o ℕ

ix: ℕ

↑f 0 + 1 ≤ ↑f (ix + 1)
OrderEmbedding.lt_iff_lt: ∀ {α : Type ?u.15651} {β : Type ?u.15650} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) {a b : α},
  ↑f a < ↑f b ↔ a < b
OrderEmbedding.lt_iff_lt
α: 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':= 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): ℕ ↪o ℕ

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':= 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): ℕ ↪o ℕ

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':= 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): ℕ ↪o ℕ

∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)exact 
ix: ℕ
ix.
succ_pos: ∀ (n : ℕ), 0 < Nat.succ n
succ_pos
Goals accomplished! 🐙
  
α: Type u_1

l, l': List α

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)

l <+ l'rw [
α: 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':= 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): ℕ ↪o ℕ

this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)

cons.intro
hd :: tl <+ l'← 
List.take_append_drop: ∀ {α : Type ?u.15874} (n : ℕ) (l : List α), take n l ++ drop n l = l
List.take_append_drop (
f: ℕ ↪o ℕ
f 
0: ?m.16022
0 + 
1: ?m.16033
1) 
l': List α
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':= 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): ℕ ↪o ℕ

this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)

cons.intro
hd :: tl <+ take (↑f 0 + 1) l' ++ drop (↑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':= 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): ℕ ↪o ℕ

this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)

cons.intro
hd :: tl <+ l'← 
List.singleton_append: ∀ {α : Type ?u.16095} {x : α} {l : List α}, [x] ++ l = x :: 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':= 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): ℕ ↪o ℕ

this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)

cons.intro
[hd] ++ tl <+ take (↑f 0 + 1) l' ++ drop (↑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':= 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): ℕ ↪o ℕ

this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)

cons.intro
[hd] ++ tl <+ take (↑f 0 + 1) l' ++ drop (↑f 0 + 1) l'
  
α: Type u_1

l, l': List α

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)

l <+ l'apply 
List.Sublist.append: ∀ {α : Type ?u.16129} {l₁ l₂ r₁ r₂ : List α}, l₁ <+ l₂ → r₁ <+ r₂ → l₁ ++ r₁ <+ l₂ ++ r₂
List.Sublist.append 
_: ?m.16131 <+ ?m.16132
_ (
IH: ?m.8441 tl
IH 
_: ℕ ↪o ℕ
_ 
this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
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':= 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): ℕ ↪o ℕ

this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)

[hd] <+ take (↑f 0 + 1) l'
  
α: Type u_1

l, l': List α

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)

l <+ l'rw [
α: 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':= 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): ℕ ↪o ℕ

this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)

[hd] <+ take (↑f 0 + 1) l'
List.singleton_sublist: ∀ {α : Type ?u.16167} {a : α} {l : List α}, [a] <+ l ↔ a ∈ l
List.singleton_sublist,
α: 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':= 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): ℕ ↪o ℕ

this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)

hd ∈ 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':= 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): ℕ ↪o ℕ

this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)

[hd] <+ take (↑f 0 + 1) l'← 
h: get l' { val := ↑f 0, isLt := w } = hd
h,
α: 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':= 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): ℕ ↪o ℕ

this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)

get l' { val := ↑f 0, isLt := w } ∈ 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':= 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): ℕ ↪o ℕ

this: ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)

[hd] <+ take (↑f 0 + 1) l'
l': List α
l'.
get_take: ∀ {α : Type ?u.16194} (L : List α) {i j : ℕ} (hi : i < length L) (hj : i < j),
  get L { val := i, isLt := hi } = get (take j L) { val := i, isLt := (_ : i < length (take j L)) }
get_take 
_: ?m.16202 < length l'
_ (
Nat.lt_succ_self: ∀ (n : ℕ), n < Nat.succ n
Nat.lt_succ_self 
_: ℕ
_)
α: 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':= 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): ℕ ↪o ℕ

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':= 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): ℕ ↪o ℕ

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)

l <+ l'apply 
List.get_mem: ∀ {α : Type ?u.16230} (l : List α) (n : ℕ) (h : n < length l), get l { val := n, isLt := h } ∈ l
List.get_mem
Goals accomplished! 🐙
#align list.sublist_of_order_embedding_nth_eq 
List.sublist_of_orderEmbedding_get?_eq: ∀ {α : Type u_1} {l l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) → l <+ l'
List.sublist_of_orderEmbedding_get?_eq

/-- A `l : List α` is `Sublist l l'` for `l' : List α` iff
there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`.
-/
theorem 
sublist_iff_exists_orderEmbedding_get?_eq: ∀ {l l' : List α}, l <+ l' ↔ ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
sublist_iff_exists_orderEmbedding_get?_eq {
l: List α
l 
l': List α
l' : 
List: Type ?u.16333 → Type ?u.16333
List 
α: Type ?u.16327
α} :
    
l: List α
l <+ 
l': List α
l' ↔ ∃ 
f: ℕ ↪o ℕ
f : 
ℕ: Type
ℕ ↪o 
ℕ: Type
ℕ, ∀ 
ix: ℕ
ix : 
ℕ: Type
ℕ, 
l: List α
l.
get?: {α : Type ?u.16355} → List α → ℕ → Option α
get? 
ix: ℕ
ix = 
l': List α
l'.
get?: {α : Type ?u.16360} → List α → ℕ → Option α
get? (
f: ℕ ↪o ℕ
f 
ix: ℕ
ix) := by
Goals accomplished! 🐙
  
α: Type u_1

l, l': List α

l <+ l' ↔ ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)constructor
α: Type u_1

l, l': List α

mp
l <+ l' → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
α: Type u_1

l, l': List α

mpr
(∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) → l <+ l'
  
α: Type u_1

l, l': List α

l <+ l' ↔ ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)·
α: Type u_1

l, l': List α

mp
l <+ l' → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix) 
α: Type u_1

l, l': List α

mp
l <+ l' → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
α: Type u_1

l, l': List α

mpr
(∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) → l <+ l'intro 
H: ?a
H
α: Type u_1

l, l': List α

H: l <+ l'

mp
∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
    
α: Type u_1

l, l': List α

mp
l <+ l' → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)induction' 
H: ?a
H with 
xs: List ?m.16583
xs 
ys: List ?m.16583
ys 
y: ?m.16583
y 
_H: xs <+ ys
_H 
IH: ?m.16584 xs ys _H
IH 
xs: List ?m.16583
xs 
ys: List ?m.16583
ys 
x: ?m.16583
x 
_H: xs <+ ys
_H 
IH: ?m.16584 xs ys _H
IH
α: Type u_1

l, l': List α

mp.slnil
∃ f, ∀ (ix : ℕ), get? [] ix = get? [] (↑f ix)
α: Type u_1

l, l', xs, ys: List α

y: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons
∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂
∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)
    
α: Type u_1

l, l': List α

mp
l <+ l' → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)·
α: Type u_1

l, l': List α

mp.slnil
∃ f, ∀ (ix : ℕ), get? [] ix = get? [] (↑f ix) 
α: Type u_1

l, l': List α

mp.slnil
∃ f, ∀ (ix : ℕ), get? [] ix = get? [] (↑f ix)
α: Type u_1

l, l', xs, ys: List α

y: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons
∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂
∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)simp
Goals accomplished! 🐙
    
α: Type u_1

l, l': List α

mp
l <+ l' → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)·
α: Type u_1

l, l', xs, ys: List α

y: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons
∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix) 
α: Type u_1

l, l', xs, ys: List α

y: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons
∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂
∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)obtain 
⟨f, hf⟩: ?m.16584 xs ys _H
⟨
f: ℕ ↪o ℕ
f
⟨f, hf⟩: ?m.16584 xs ys _H
, 
hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
hf
⟨f, hf⟩: ?m.16584 xs ys _H
⟩ := 
IH: ?m.16584 xs ys _H
IH
α: Type u_1

l, l', xs, ys: List α

y: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons.intro
∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)
      
α: Type u_1

l, l', xs, ys: List α

y: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons
∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)refine' ⟨
f: ℕ ↪o ℕ
f.
trans: {α : Type ?u.17404} →
  {β : Type ?u.17403} →
    {γ : Type ?u.17402} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ↪r s → s ↪r t → r ↪r t
trans (
OrderEmbedding.ofStrictMono: {α : Type ?u.17434} →
  {β : Type ?u.17433} → [inst : LinearOrder α] → [inst_1 : Preorder β] → (f : α → β) → StrictMono f → α ↪o β
OrderEmbedding.ofStrictMono 
(· + 1): ℕ → ℕ
(· + 1) fun 
_: ?m.17616
_ => 
α: Type u_1

l, l', xs, ys: List α

y: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons.intro
∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)by
Goals accomplished! 🐙 
α: Type u_1

l, l', xs, ys: List α

y: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

x✝: ℕ

∀ ⦃b : ℕ⦄, x✝ < b → (fun x => x + 1) x✝ < (fun x => x + 1) bsimp
Goals accomplished! 🐙), 
_: ?m.17397
  (RelEmbedding.trans f
    (OrderEmbedding.ofStrictMono (fun x => x + 1)
      (_ : ∀ (x : ℕ) ⦃b : ℕ⦄, x < b → (fun x => x + 1) x < (fun x => x + 1) b)))
_⟩
α: Type u_1

l, l', xs, ys: List α

y: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons.intro
∀ (ix : ℕ),
  get? xs ix =     get? (y :: ys)
      (↑(RelEmbedding.trans f (OrderEmbedding.ofStrictMono (fun x => x + 1) (_ : ∀ (x a : ℕ), x < a → x + 1 < a + 1)))
        ix)
      
α: Type u_1

l, l', xs, ys: List α

y: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons
∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)simpa using 
hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
hf
Goals accomplished! 🐙
    
α: Type u_1

l, l': List α

mp
l <+ l' → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)·
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂
∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix) 
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂
∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)obtain 
⟨f, hf⟩: ?m.16584 xs ys _H
⟨
f: ℕ ↪o ℕ
f
⟨f, hf⟩: ?m.16584 xs ys _H
, 
hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
hf
⟨f, hf⟩: ?m.16584 xs ys _H
⟩ := 
IH: ?m.16584 xs ys _H
IH
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro
∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)
      
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂
∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)refine'
        ⟨
OrderEmbedding.ofMapLEIff: {α : Type ?u.44127} →
  {β : Type ?u.44126} →
    [inst : PartialOrder α] → [inst_1 : Preorder β] → (f : α → β) → (∀ (a b : α), f a ≤ f b ↔ a ≤ b) → α ↪o β
OrderEmbedding.ofMapLEIff (fun 
ix: ℕ
ix : 
ℕ: Type
ℕ => if 
ix: ℕ
ix = 
0: ?m.44194
0 then 
0: ?m.44225
0 else (
f: ℕ ↪o ℕ
f 
ix: ℕ
ix.
pred: ℕ → ℕ
pred).
succ: ℕ → ℕ
succ) 
_: ∀ (a b : ?m.44128),
  (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤       (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔     a ≤ b
_, 
_: ?m.44124
  (OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) ?mp.cons₂.intro.refine'_1)
_⟩
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_1
∀ (a b : ℕ),
  (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤       (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔     a ≤ b
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_2
∀ (ix : ℕ),
  get? (x :: xs) ix =     get? (x :: ys)
      (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
            ?mp.cons₂.intro.refine'_1)
        ix)
      
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂
∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)·
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_1
∀ (a b : ℕ),
  (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤       (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔     a ≤ b 
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_1
∀ (a b : ℕ),
  (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤       (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔     a ≤ b
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_2
∀ (ix : ℕ),
  get? (x :: xs) ix =     get? (x :: ys)
      (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
            ?mp.cons₂.intro.refine'_1)
        ix)rintro 
⟨_ | a⟩: ?m.44128
⟨_ | a⟩ 
⟨_ | b⟩: ℕ
⟨_ | b⟩
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_1.zero.zero
(fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ≤     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ↔   Nat.zero ≤ Nat.zero
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

n✝: ℕ

mp.cons₂.intro.refine'_1.zero.succ
(fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ≤     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝) ↔   Nat.zero ≤ Nat.succ n✝
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

n✝: ℕ

mp.cons₂.intro.refine'_1.succ.zero
(fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝) ≤     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ↔   Nat.succ n✝ ≤ Nat.zero
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

n✝¹, n✝: ℕ

mp.cons₂.intro.refine'_1.succ.succ
(fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝¹) ≤     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝) ↔   Nat.succ n✝¹ ≤ Nat.succ n✝ 
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_1
∀ (a b : ℕ),
  (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤       (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔     a ≤ b<;>
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_1.zero.zero
(fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ≤     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ↔   Nat.zero ≤ Nat.zero
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

n✝: ℕ

mp.cons₂.intro.refine'_1.zero.succ
(fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ≤     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝) ↔   Nat.zero ≤ Nat.succ n✝
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

n✝: ℕ

mp.cons₂.intro.refine'_1.succ.zero
(fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝) ≤     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ↔   Nat.succ n✝ ≤ Nat.zero
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

n✝¹, n✝: ℕ

mp.cons₂.intro.refine'_1.succ.succ
(fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝¹) ≤     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝) ↔   Nat.succ n✝¹ ≤ Nat.succ n✝ 
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_1
∀ (a b : ℕ),
  (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤       (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔     a ≤ bsimp [
Nat.succ_le_succ_iff: ∀ {a b : ℕ}, Nat.succ a ≤ Nat.succ b ↔ a ≤ b
Nat.succ_le_succ_iff]
Goals accomplished! 🐙
      
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

IH: ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂
∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)·
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_2
∀ (ix : ℕ),
  get? (x :: xs) ix =     get? (x :: ys)
      (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
            (_ :
              ∀ (a b : ℕ),
                (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤                     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔                   a ≤ b))
        ix) 
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_2
∀ (ix : ℕ),
  get? (x :: xs) ix =     get? (x :: ys)
      (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
            (_ :
              ∀ (a b : ℕ),
                (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤                     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔                   a ≤ b))
        ix)rintro 
⟨_ | i⟩: ℕ
⟨_ | i⟩
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_2.zero
get? (x :: xs) Nat.zero =   get? (x :: ys)
    (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
          (_ :
            ∀ (a b : ℕ),
              (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤                   (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔                 a ≤ b))
      Nat.zero)
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

n✝: ℕ

mp.cons₂.intro.refine'_2.succ
get? (x :: xs) (Nat.succ n✝) =   get? (x :: ys)
    (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
          (_ :
            ∀ (a b : ℕ),
              (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤                   (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔                 a ≤ b))
      (Nat.succ n✝))
        
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_2
∀ (ix : ℕ),
  get? (x :: xs) ix =     get? (x :: ys)
      (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
            (_ :
              ∀ (a b : ℕ),
                (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤                     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔                   a ≤ b))
        ix)·
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_2.zero
get? (x :: xs) Nat.zero =   get? (x :: ys)
    (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
          (_ :
            ∀ (a b : ℕ),
              (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤                   (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔                 a ≤ b))
      Nat.zero) 
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_2.zero
get? (x :: xs) Nat.zero =   get? (x :: ys)
    (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
          (_ :
            ∀ (a b : ℕ),
              (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤                   (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔                 a ≤ b))
      Nat.zero)
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

n✝: ℕ

mp.cons₂.intro.refine'_2.succ
get? (x :: xs) (Nat.succ n✝) =   get? (x :: ys)
    (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
          (_ :
            ∀ (a b : ℕ),
              (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤                   (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔                 a ≤ b))
      (Nat.succ n✝))simp
Goals accomplished! 🐙
        
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

mp.cons₂.intro.refine'_2
∀ (ix : ℕ),
  get? (x :: xs) ix =     get? (x :: ys)
      (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
            (_ :
              ∀ (a b : ℕ),
                (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤                     (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔                   a ≤ b))
        ix)·
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

n✝: ℕ

mp.cons₂.intro.refine'_2.succ
get? (x :: xs) (Nat.succ n✝) =   get? (x :: ys)
    (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
          (_ :
            ∀ (a b : ℕ),
              (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤                   (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔                 a ≤ b))
      (Nat.succ n✝)) 
α: Type u_1

l, l', xs, ys: List α

x: α

_H: xs <+ ys

f: ℕ ↪o ℕ

hf: ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)

n✝: ℕ

mp.cons₂.intro.refine'_2.succ
get? (x ::