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

case mpr
α : Type u_1
l l' : List α
⊢ (∃ 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)
constructor
case mp
α : Type u_1
l l' : List α
H : l <+ l'
⊢ ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
case mp
α : Type u_1
l l' : List α
⊢ l <+ l' → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
intro H
case mp.slnil
α : Type u_1
l l' : List α
⊢ ∃ f, ∀ (ix : ℕ), get? [] ix = get? [] (↑f ix)

case mp.cons
α : Type u_1
l l' xs ys : List α
y : α
_H : xs <+ ys
IH : ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)

case mp.cons₂
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
IH : ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)
case mp
α : Type u_1
l l' : List α
H : l <+ l'
⊢ ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
induction' H with xs ys y _H IH xs ys x _H IH
no goals
case mp.slnil
α : Type u_1
l l' : List α
⊢ ∃ f, ∀ (ix : ℕ), get? [] ix = get? [] (↑f ix)
simp
case mp.cons.intro
α : Type u_1
l l' xs ys : List α
y : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)
case mp.cons
α : Type u_1
l l' xs ys : List α
y : α
_H : xs <+ ys
IH : ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)
obtain ⟨f, hf⟩ := IH
no goals
case mp.cons.intro
α : Type u_1
l l' xs ys : List α
y : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∀ (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)
simpa using hf
no goals
α : 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) b
simp
case mp.cons₂.intro
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)
case mp.cons₂
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
IH : ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)
obtain ⟨f, hf⟩ := IH
case 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)
⊢ ∀ (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

case mp.cons₂.intro.refine'_2
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∀ (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)
case mp.cons₂.intro
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)
refine'
  ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) _, _⟩
no goals
case 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)
⊢ ∀ (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
rintro ⟨_ | a⟩ ⟨_ | b⟩ <;> simp [Nat.succ_le_succ_iff]
case mp.cons₂.intro.refine'_2.zero
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ 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)

case mp.cons₂.intro.refine'_2.succ
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
n✝ : ℕ
⊢ 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✝))
case mp.cons₂.intro.refine'_2
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∀ (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⟩
no goals
case mp.cons₂.intro.refine'_2.zero
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ 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)
simp
no goals
case mp.cons₂.intro.refine'_2.succ
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
n✝ : ℕ
⊢ 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✝))
simpa using hf _
case mpr.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
⊢ l <+ l'
case mpr
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) → l <+ l'
rintro ⟨f, hf⟩
no goals
case mpr.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
⊢ l <+ l'
exact sublist_of_orderEmbedding_get?_eq f hf