-- Mathlib/Data/List/NodupEquivFin.lean
theorem sublist_iff_exists_orderEmbedding_getElem?_eq {l l' : List α} :
    l <+ l' ↔ ∃ f : ℕ ↪o ℕ, ∀ ix : ℕ, l[ix]? = l'[f ix]?

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

Tactic:
intro H

Result:
case mp
α : Type u_1
l l' : List α
H : l <+ l'
⊢ ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

Proof state:
case mp.cons₂.intro.refine_2.zero
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ (a✝¹ :: l₁✝)[0]? = (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else (f ix.pred).succ) ⋯) 0]?

Tactic:
simp

Result:
no goals

Proof state:
case mp.cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH : ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = (a✝¹ :: l₂✝)[f ix]?

Tactic:
obtain ⟨f, hf⟩ := IH

Result:
case mp.cons.intro
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = (a✝¹ :: l₂✝)[f ix]?

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

Tactic:
simp

Result:
no goals

Proof state:
case mp.cons₂.intro.refine_2.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ (a✝¹ :: l₁✝)[n✝ + 1]? =
    (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else (f ix.pred).succ) ⋯) (n✝ + 1)]?

Tactic:
simpa using hf _

Result:
no goals

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

Tactic:
rintro ⟨f, hf⟩

Result:
case mpr.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
⊢ l <+ l'

Proof state:
case mp.cons₂
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH : ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), (a✝¹ :: l₁✝)[ix]? = (a✝¹ :: l₂✝)[f ix]?

Tactic:
obtain ⟨f, hf⟩ := IH

Result:
case mp.cons₂.intro
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), (a✝¹ :: l₁✝)[ix]? = (a✝¹ :: l₂✝)[f ix]?

Proof state:
α : Type u_1
l l' : List α
⊢ l <+ l' ↔ ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

Tactic:
constructor

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

case mpr
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?) → l <+ l'

Proof state:
case mp.cons₂.intro
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), (a✝¹ :: l₁✝)[ix]? = (a✝¹ :: l₂✝)[f ix]?

Tactic:
refine
  ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩

Result:
case mp.cons₂.intro.refine_1
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (a b : ℕ),
    (fun ix => if ix = 0 then 0 else (f ix.pred).succ) a ≤ (fun ix => if ix = 0 then 0 else (f ix.pred).succ) b ↔ a ≤ b

case mp.cons₂.intro.refine_2
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (ix : ℕ),
    (a✝¹ :: l₁✝)[ix]? =
      (a✝¹ ::
          l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else (f ix.pred).succ) ?mp.cons₂.intro.refine_1)
          ix]?

Proof state:
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
x✝ : ℕ
⊢ ∀ ⦃b : ℕ⦄, x✝ < b → (fun x => x + 1) x✝ < (fun x => x + 1) b

Tactic:
simp

Result:
no goals

Proof state:
case mp.cons.intro
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (ix : ℕ), l₁✝[ix]? = (a✝¹ :: l₂✝)[(RelEmbedding.trans f (OrderEmbedding.ofStrictMono (fun x => x + 1) ⋯)) ix]?

Tactic:
simpa using hf

Result:
no goals

Proof state:
case mp.cons₂.intro.refine_1
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (a b : ℕ),
    (fun ix => if ix = 0 then 0 else (f ix.pred).succ) a ≤ (fun ix => if ix = 0 then 0 else (f ix.pred).succ) b ↔ a ≤ b

Tactic:
rintro ⟨_ | a⟩ ⟨_ | b⟩ <;> simp [Nat.succ_le_succ_iff]

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
⊢ l <+ l'

Tactic:
exact sublist_of_orderEmbedding_getElem?_eq f hf

Result:
no goals

Proof state:
case mp.cons₂.intro.refine_2
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (ix : ℕ),
    (a✝¹ :: l₁✝)[ix]? =
      (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else (f ix.pred).succ) ⋯) ix]?

Tactic:
rintro ⟨_ | i⟩

Result:
case mp.cons₂.intro.refine_2.zero
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ (a✝¹ :: l₁✝)[0]? = (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else (f ix.pred).succ) ⋯) 0]?

case mp.cons₂.intro.refine_2.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ (a✝¹ :: l₁✝)[n✝ + 1]? =
    (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else (f ix.pred).succ) ⋯) (n✝ + 1)]?