-- Mathlib/Data/List/NodupEquivFin.lean
theorem sublist_iff_exists_fin_orderEmbedding_get_eq {l l' : List α} :
    l <+ l' ↔
      ∃ f : Fin l.length ↪o Fin l'.length,
        ∀ ix : Fin l.length, l.get ix = l'.get (f ix)

Proof state:
case mp.intro.refine_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
⊢ ∀ (ix : Fin l.length), l.get ix = l'.get ((OrderEmbedding.ofMapLEIff (fun ix => ⟨f ↑ix, ⋯⟩) ⋯) ix)

Tactic:
intro i

Result:
case mp.intro.refine_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
i : Fin l.length
⊢ l.get i = l'.get ((OrderEmbedding.ofMapLEIff (fun ix => ⟨f ↑ix, ⋯⟩) ⋯) i)

Proof state:
case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i : ℕ
hi : i < l.length
⊢ l[i]? = l'[↑(f ⟨i, hi⟩)]?

Tactic:
specialize hf ⟨i, hi⟩

Result:
case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
i : ℕ
hi : i < l.length
hf : l.get ⟨i, hi⟩ = l'.get (f ⟨i, hi⟩)
⊢ l[i]? = l'[↑(f ⟨i, hi⟩)]?

Proof state:
case mp.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
⊢ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Tactic:
have h : ∀ {i : ℕ}, i < l.length → f i < l'.length := by
  intro i hi
  specialize hf i
  rw [getElem?_eq_getElem hi, eq_comm, getElem?_eq_some_iff] at hf
  obtain ⟨h, -⟩ := hf
  exact h

Result:
case mp.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
⊢ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Proof state:
case mpr.intro.refine_2
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i : ℕ
⊢ l[i]? = l'[if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length]?

Tactic:
split_ifs with hi

Result:
case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i : ℕ
hi : i < l.length
⊢ l[i]? = l'[↑(f ⟨i, hi⟩)]?

case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i : ℕ
hi : ¬i < l.length
⊢ l[i]? = l'[i + l'.length]?

Proof state:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
hf : ∃ (h : f i < l'.length), l'[f i] = l[i]
⊢ f i < l'.length

Tactic:
obtain ⟨h, -⟩ := hf

Result:
case intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
h : f i < l'.length
⊢ f i < l'.length

Proof state:
case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : i < l.length
hj : j < l.length
⊢ ↑(f ⟨i, hi⟩) < ↑(f ⟨j, hj⟩)

Tactic:
rwa [Fin.val_fin_lt, f.lt_iff_lt]

Result:
no goals

Proof state:
α : Type u_1
l l' : List α
⊢ l <+ l' ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Tactic:
rw [sublist_iff_exists_orderEmbedding_getElem?_eq]

Result:
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?) ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Proof state:
case mp
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?) → ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Tactic:
rintro ⟨f, hf⟩

Result:
case mp.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
⊢ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Proof state:
case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : ¬j < l.length
⊢ i + l'.length < j + l'.length

Tactic:
simpa using h

Result:
no goals

Proof state:
case mp.intro.refine_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
i : Fin l.length
⊢ l.get i = l'.get ((OrderEmbedding.ofMapLEIff (fun ix => ⟨f ↑ix, ⋯⟩) ⋯) i)

Tactic:
apply Option.some_injective

Result:
case mp.intro.refine_2.a
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
i : Fin l.length
⊢ some (l.get i) = some (l'.get ((OrderEmbedding.ofMapLEIff (fun ix => ⟨f ↑ix, ⋯⟩) ⋯) i))

Proof state:
case mpr.intro.refine_2
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
⊢ ∀ (ix : ℕ),
    l[ix]? =
      l'[(OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) ⋯) ix]?

Tactic:
intro i

Result:
case mpr.intro.refine_2
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i : ℕ
⊢ l[i]? = l'[(OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) ⋯) i]?

Proof state:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
hf : l[i]? = l'[f i]?
⊢ f i < l'.length

Tactic:
rw [getElem?_eq_getElem hi, eq_comm, getElem?_eq_some_iff] at hf

Result:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
hf : ∃ (h : f i < l'.length), l'[f i] = l[i]
⊢ f i < l'.length

Proof state:
case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : j < l.length
⊢ i + l'.length < ↑(f ⟨j, hj⟩)

Tactic:
exact absurd (h.trans hj) hi

Result:
no goals

Proof state:
case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i : ℕ
hi : ¬i < l.length
⊢ l'.length ≤ i + l'.length

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.refine_1
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
⊢ (fun i => if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) i <
    (fun i => if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) j

Tactic:
dsimp only

Result:
case mpr.intro.refine_1
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
⊢ (if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) <
    if hi : j < l.length then ↑(f ⟨j, hi⟩) else j + l'.length