α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) ↔ ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
α : Type u_1
l l' : List α
⊢ l <+ l' ↔ ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
rw [sublist_iff_exists_orderEmbedding_get?_eq]
case mp
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) → ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)

case mpr
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)) → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) ↔ ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
constructor
case mp.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
⊢ ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
case mp
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) → ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
rintro ⟨f, hf⟩
case mp.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
⊢ ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
case mp.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
⊢ ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
have h : ∀ {i : ℕ} (_ : i < l.length), f i < l'.length := by
  intro i hi
  specialize hf i
  rw [get?_eq_get hi, eq_comm, get?_eq_some] at hf
  obtain ⟨h, -⟩ := hf
  exact h
case mp.intro.refine'_1
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
⊢ ∀ (a b : Fin (length l)),
    (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') }) a ≤
        (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') }) b ↔
      a ≤ b

case mp.intro.refine'_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
⊢ ∀ (ix : Fin (length l)),
    get l ix =
      get l'
        (↑(OrderEmbedding.ofMapLEIff (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') })
              ?mp.intro.refine'_1)
          ix)
case mp.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
⊢ ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
refine' ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) _, _⟩
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
i : ℕ
hi : i < length l
⊢ ↑f i < length l'
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
⊢ ∀ {i : ℕ}, i < length l → ↑f i < length l'
intro i hi
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < length l
hf : get? l i = get? l' (↑f i)
⊢ ↑f i < length l'
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
i : ℕ
hi : i < length l
⊢ ↑f i < length l'
specialize hf i
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < length l
hf : ∃ h, get l' { val := ↑f i, isLt := h } = get l { val := i, isLt := hi }
⊢ ↑f i < length l'
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < length l
hf : get? l i = get? l' (↑f i)
⊢ ↑f i < length l'
rw [get?_eq_get hi, eq_comm, get?_eq_some] at hf
case intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < length l
h : ↑f i < length l'
⊢ ↑f i < length l'
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < length l
hf : ∃ h, get l' { val := ↑f i, isLt := h } = get l { val := i, isLt := hi }
⊢ ↑f i < length l'
obtain ⟨h, -⟩ := hf
no goals
case intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < length l
h : ↑f i < length l'
⊢ ↑f i < length l'
exact h
no goals
case mp.intro.refine'_1
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
⊢ ∀ (a b : Fin (length l)),
    (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') }) a ≤
        (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') }) b ↔
      a ≤ b
simp
case mp.intro.refine'_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
i : Fin (length l)
⊢ get l i =
    get l'
      (↑(OrderEmbedding.ofMapLEIff (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') })
            (_ :
              ∀ (a a_1 : Fin (length l)),
                { val := ↑f ↑a, isLt := (_ : ↑f ↑a < length l') } ≤
                    { val := ↑f ↑a_1, isLt := (_ : ↑f ↑a_1 < length l') } ↔
                  a ≤ a_1))
        i)
case mp.intro.refine'_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
⊢ ∀ (ix : Fin (length l)),
    get l ix =
      get l'
        (↑(OrderEmbedding.ofMapLEIff (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') })
              (_ :
                ∀ (a a_1 : Fin (length l)),
                  { val := ↑f ↑a, isLt := (_ : ↑f ↑a < length l') } ≤
                      { val := ↑f ↑a_1, isLt := (_ : ↑f ↑a_1 < length l') } ↔
                    a ≤ a_1))
          ix)
intro i
case mp.intro.refine'_2.a
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
i : Fin (length l)
⊢ some (get l i) =
    some
      (get l'
        (↑(OrderEmbedding.ofMapLEIff (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') })
              (_ :
                ∀ (a a_1 : Fin (length l)),
                  { val := ↑f ↑a, isLt := (_ : ↑f ↑a < length l') } ≤
                      { val := ↑f ↑a_1, isLt := (_ : ↑f ↑a_1 < length l') } ↔
                    a ≤ a_1))
          i))
case mp.intro.refine'_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
i : Fin (length l)
⊢ get l i =
    get l'
      (↑(OrderEmbedding.ofMapLEIff (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') })
            (_ :
              ∀ (a a_1 : Fin (length l)),
                { val := ↑f ↑a, isLt := (_ : ↑f ↑a < length l') } ≤
                    { val := ↑f ↑a_1, isLt := (_ : ↑f ↑a_1 < length l') } ↔
                  a ≤ a_1))
        i)
apply Option.some_injective
no goals
case mp.intro.refine'_2.a
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
i : Fin (length l)
⊢ some (get l i) =
    some
      (get l'
        (↑(OrderEmbedding.ofMapLEIff (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') })
              (_ :
                ∀ (a a_1 : Fin (length l)),
                  { val := ↑f ↑a, isLt := (_ : ↑f ↑a < length l') } ≤
                      { val := ↑f ↑a_1, isLt := (_ : ↑f ↑a_1 < length l') } ↔
                    a ≤ a_1))
          i))
simpa [get?_eq_get i.2, get?_eq_get (h i.2)] using hf i
case mpr.intro
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
case mpr
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)) → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
rintro ⟨f, hf⟩
case mpr.intro.refine'_1
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
⊢ StrictMono fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l'

case mpr.intro.refine'_2
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
⊢ ∀ (ix : ℕ),
    get? l ix =
      get? l'
        (↑(OrderEmbedding.ofStrictMono
              (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l')
              ?mpr.intro.refine'_1)
          ix)
case mpr.intro
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
refine'
  ⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length)
      _,
    _⟩
case mpr.intro.refine'_1
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
⊢ (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') i <
    (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') j
case mpr.intro.refine'_1
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
⊢ StrictMono fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l'
intro i j h
case mpr.intro.refine'_1
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
⊢ (if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') <
    if hi : j < length l then ↑(↑f { val := j, isLt := hi }) else j + length l'
case mpr.intro.refine'_1
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
⊢ (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') i <
    (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') j
dsimp only
case mpr.intro.refine'_1.inl.inl
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : i < length l
hj : j < length l
⊢ ↑(↑f { val := i, isLt := hi }) < ↑(↑f { val := j, isLt := hj })

case mpr.intro.refine'_1.inl.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : i < length l
hj : ¬j < length l
⊢ ↑(↑f { val := i, isLt := hi }) < j + length l'

case mpr.intro.refine'_1.inr.inl
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : ¬i < length l
hj : j < length l
⊢ i + length l' < ↑(↑f { val := j, isLt := hj })

case mpr.intro.refine'_1.inr.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : ¬i < length l
hj : ¬j < length l
⊢ i + length l' < j + length l'
case mpr.intro.refine'_1
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
⊢ (if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') <
    if hi : j < length l then ↑(↑f { val := j, isLt := hi }) else j + length l'
split_ifs with hi hj hj
no goals
case mpr.intro.refine'_1.inl.inl
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : i < length l
hj : j < length l
⊢ ↑(↑f { val := i, isLt := hi }) < ↑(↑f { val := j, isLt := hj })
rwa [Fin.val_fin_lt, f.lt_iff_lt]
case mpr.intro.refine'_1.inl.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : i < length l
hj : ¬j < length l
⊢ ↑(↑f { val := i, isLt := hi }) < length l' + j
case mpr.intro.refine'_1.inl.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : i < length l
hj : ¬j < length l
⊢ ↑(↑f { val := i, isLt := hi }) < j + length l'
rw [add_comm]
no goals
case mpr.intro.refine'_1.inl.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : i < length l
hj : ¬j < length l
⊢ ↑(↑f { val := i, isLt := hi }) < length l' + j
exact lt_add_of_lt_of_pos (Fin.is_lt _) (i.zero_le.trans_lt h)
no goals
case mpr.intro.refine'_1.inr.inl
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : ¬i < length l
hj : j < length l
⊢ i + length l' < ↑(↑f { val := j, isLt := hj })
exact absurd (h.trans hj) hi
no goals
case mpr.intro.refine'_1.inr.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : ¬i < length l
hj : ¬j < length l
⊢ i + length l' < j + length l'
simpa using h
case mpr.intro.refine'_2
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
⊢ get? l i =
    get? l'
      (↑(OrderEmbedding.ofStrictMono
            (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l')
            (_ :
              ∀ ⦃i j : ℕ⦄,
                i < j →
                  (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') i <
                    (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') j))
        i)
case mpr.intro.refine'_2
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
⊢ ∀ (ix : ℕ),
    get? l ix =
      get? l'
        (↑(OrderEmbedding.ofStrictMono
              (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l')
              (_ :
                ∀ ⦃i j : ℕ⦄,
                  i < j →
                    (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') i <
                      (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') j))
          ix)
intro i
case mpr.intro.refine'_2
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
⊢ get? l i = get? l' (if h : i < length l then ↑(↑f { val := i, isLt := (_ : i < length l) }) else i + length l')
case mpr.intro.refine'_2
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
⊢ get? l i =
    get? l'
      (↑(OrderEmbedding.ofStrictMono
            (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l')
            (_ :
              ∀ ⦃i j : ℕ⦄,
                i < j →
                  (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') i <
                    (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') j))
        i)
simp only [OrderEmbedding.coe_ofStrictMono]
case mpr.intro.refine'_2.inl
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : i < length l
⊢ get? l i = get? l' ↑(↑f { val := i, isLt := (_ : i < length l) })

case mpr.intro.refine'_2.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : ¬i < length l
⊢ get? l i = get? l' (i + length l')
case mpr.intro.refine'_2
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
⊢ get? l i = get? l' (if h : i < length l then ↑(↑f { val := i, isLt := (_ : i < length l) }) else i + length l')
split_ifs with hi
no goals
case mpr.intro.refine'_2.inl
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : i < length l
⊢ get? l i = get? l' ↑(↑f { val := i, isLt := (_ : i < length l) })
rw [get?_eq_get hi, get?_eq_get, ← hf]
case mpr.intro.refine'_2.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : ¬i < length l
⊢ length l' ≤ i + length l'

case mpr.intro.refine'_2.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : ¬i < length l
⊢ length l ≤ i
case mpr.intro.refine'_2.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : ¬i < length l
⊢ get? l i = get? l' (i + length l')
rw [get?_eq_none.mpr, get?_eq_none.mpr]
no goals
case mpr.intro.refine'_2.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : ¬i < length l
⊢ length l' ≤ i + length l'
simp
no goals
case mpr.intro.refine'_2.inr
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : ¬i < length l
⊢ length l ≤ i
simpa using hi