-- 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 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)
⊢ StrictMono fun i => if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length

Tactic:
intro i j h

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
⊢ (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

Proof state:
case mpr.intro
α : 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)
⊢ ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

Tactic:
refine
  ⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length)
      ?_,
    ?_⟩

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)
⊢ StrictMono fun i => if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length

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)
            ?mpr.intro.refine_1)
          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'[(OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) ⋯) i]?

Tactic:
simp only [OrderEmbedding.coe_ofStrictMono]

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'[if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length]?

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

Tactic:
specialize hf i

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

Proof state:
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⟩)]?

Tactic:
simp_all

Result:
no goals

Proof state:
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))

Tactic:
simpa [getElem?_eq_getElem i.2, getElem?_eq_getElem (h i.2)] using hf i

Result:
no goals

Proof state:
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)

Tactic:
refine ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) ?_, ?_⟩

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

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, ⋯⟩) ?mp.intro.refine_1) ix)

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

Tactic:
exact h

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
⊢ ∀ {i : ℕ}, i < l.length → f i < l'.length

Tactic:
intro i hi

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

Proof state:
α : 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:
constructor

Result:
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)

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

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

Tactic:
rintro ⟨f, hf⟩

Result:
case mpr.intro
α : 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)
⊢ ∃ f, ∀ (ix : ℕ), l[ix]? = l'[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 : ℕ
hi : ¬i < l.length
⊢ l.length ≤ i

Tactic:
simpa using hi

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
⊢ (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

Tactic:
split_ifs with hi hj hj

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 j : ℕ
h : i < j
hi : i < l.length
hj : j < l.length
⊢ ↑(f ⟨i, hi⟩) < ↑(f ⟨j, hj⟩)

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
⊢ ↑(f ⟨i, hi⟩) < j + l'.length

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⟩)

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

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
⊢ ↑(f ⟨i, hi⟩) < j + l'.length

Tactic:
omega

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[i]? = l'[i + l'.length]?

Tactic:
rw [getElem?_eq_none_iff.mpr, getElem?_eq_none_iff.mpr]

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

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