-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isPrefix_iff_getElem {l₁ l₂ : List α} :
    l₁ <+: l₂ ↔ ∃ (h : l₁.length ≤ l₂.length), ∀ x (hx : x < l₁.length),
      l₁[x] = l₂[x]'(Nat.lt_of_lt_of_le hx h) where
  mp h := ⟨h.length_le, fun _ h' ↦ h.getElem h'⟩
  mpr h

Proof state:
case intro.cons.cons
α : Type u_1
head✝¹ : α
tail✝¹ : List α
tail_ih :
  ∀ {l₁ : List α} (hl : l₁.length ≤ tail✝¹.length),
    (∀ (x : Nat) (hx : x < l₁.length), l₁[x] = tail✝¹[x]) → l₁ <+: tail✝¹
head✝ : α
tail✝ : List α
hl : (head✝ :: tail✝).length ≤ (head✝¹ :: tail✝¹).length
h : ∀ (x : Nat) (hx : x < (head✝ :: tail✝).length), (head✝ :: tail✝)[x] = (head✝¹ :: tail✝¹)[x]
⊢ head✝ :: tail✝ <+: head✝¹ :: tail✝¹

Tactic:
simp only [length_cons, Nat.add_le_add_iff_right, Fin.getElem_fin] at hl h

Result:
case intro.cons.cons
α : Type u_1
head✝¹ : α
tail✝¹ : List α
tail_ih :
  ∀ {l₁ : List α} (hl : l₁.length ≤ tail✝¹.length),
    (∀ (x : Nat) (hx : x < l₁.length), l₁[x] = tail✝¹[x]) → l₁ <+: tail✝¹
head✝ : α
tail✝ : List α
hl✝ : (head✝ :: tail✝).length ≤ (head✝¹ :: tail✝¹).length
h : ∀ (x : Nat) (hx : x < tail✝.length + 1), (head✝ :: tail✝)[x] = (head✝¹ :: tail✝¹)[x]
hl : tail✝.length ≤ tail✝¹.length
⊢ head✝ :: tail✝ <+: head✝¹ :: tail✝¹

Proof state:
α : Type u_1
l₁ l₂ : List α
h : ∃ h, ∀ (x : Nat) (hx : x < l₁.length), l₁[x] = l₂[x]
⊢ l₁ <+: l₂

Tactic:
obtain ⟨hl, h⟩ := h

Result:
case intro
α : Type u_1
l₁ l₂ : List α
hl : l₁.length ≤ l₂.length
h : ∀ (x : Nat) (hx : x < l₁.length), l₁[x] = l₂[x]
⊢ l₁ <+: l₂

Proof state:
case intro.cons.cons
α : Type u_1
head✝¹ : α
tail✝¹ : List α
tail_ih :
  ∀ {l₁ : List α} (hl : l₁.length ≤ tail✝¹.length),
    (∀ (x : Nat) (hx : x < l₁.length), l₁[x] = tail✝¹[x]) → l₁ <+: tail✝¹
head✝ : α
tail✝ : List α
hl✝ : (head✝ :: tail✝).length ≤ (head✝¹ :: tail✝¹).length
h : ∀ (x : Nat) (hx : x < tail✝.length + 1), (head✝ :: tail✝)[x] = (head✝¹ :: tail✝¹)[x]
hl : tail✝.length ≤ tail✝¹.length
⊢ head✝ :: tail✝ <+: head✝¹ :: tail✝¹

Tactic:
simp only [cons_prefix_cons]

Result:
case intro.cons.cons
α : Type u_1
head✝¹ : α
tail✝¹ : List α
tail_ih :
  ∀ {l₁ : List α} (hl : l₁.length ≤ tail✝¹.length),
    (∀ (x : Nat) (hx : x < l₁.length), l₁[x] = tail✝¹[x]) → l₁ <+: tail✝¹
head✝ : α
tail✝ : List α
hl✝ : (head✝ :: tail✝).length ≤ (head✝¹ :: tail✝¹).length
h : ∀ (x : Nat) (hx : x < tail✝.length + 1), (head✝ :: tail✝)[x] = (head✝¹ :: tail✝¹)[x]
hl : tail✝.length ≤ tail✝¹.length
⊢ head✝ = head✝¹ ∧ tail✝ <+: tail✝¹

Proof state:
case intro
α : Type u_1
l₁ l₂ : List α
hl : l₁.length ≤ l₂.length
h : ∀ (x : Nat) (hx : x < l₁.length), l₁[x] = l₂[x]
⊢ l₁ <+: l₂

Tactic:
induction l₂ generalizing l₁ with
| nil =>
  simpa using hl
| cons _ _ tail_ih =>
  cases l₁ with
  | nil =>
    exact nil_prefix
  | cons _ _ =>
    simp only [length_cons, Nat.add_le_add_iff_right, Fin.getElem_fin] at hl h
    simp only [cons_prefix_cons]
    exact ⟨h 0 (zero_lt_succ _), tail_ih hl fun a ha ↦ h a.succ (succ_lt_succ ha)⟩

Result:
no goals

Proof state:
case intro.cons.nil
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih :
  ∀ {l₁ : List α} (hl : l₁.length ≤ tail✝.length), (∀ (x : Nat) (hx : x < l₁.length), l₁[x] = tail✝[x]) → l₁ <+: tail✝
hl : [].length ≤ (head✝ :: tail✝).length
h : ∀ (x : Nat) (hx : x < [].length), [][x] = (head✝ :: tail✝)[x]
⊢ [] <+: head✝ :: tail✝

Tactic:
exact nil_prefix

Result:
no goals

Proof state:
case intro.cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih :
  ∀ {l₁ : List α} (hl : l₁.length ≤ tail✝.length), (∀ (x : Nat) (hx : x < l₁.length), l₁[x] = tail✝[x]) → l₁ <+: tail✝
l₁ : List α
hl : l₁.length ≤ (head✝ :: tail✝).length
h : ∀ (x : Nat) (hx : x < l₁.length), l₁[x] = (head✝ :: tail✝)[x]
⊢ l₁ <+: head✝ :: tail✝

Tactic:
cases l₁ with
| nil =>
  exact nil_prefix
| cons _ _ =>
  simp only [length_cons, Nat.add_le_add_iff_right, Fin.getElem_fin] at hl h
  simp only [cons_prefix_cons]
  exact ⟨h 0 (zero_lt_succ _), tail_ih hl fun a ha ↦ h a.succ (succ_lt_succ ha)⟩

Result:
no goals

Proof state:
case intro.nil
α : Type u_1
l₁ : List α
hl : l₁.length ≤ [].length
h : ∀ (x : Nat) (hx : x < l₁.length), l₁[x] = [][x]
⊢ l₁ <+: []

Tactic:
simpa using hl

Result:
no goals

Proof state:
case intro.cons.cons
α : Type u_1
head✝¹ : α
tail✝¹ : List α
tail_ih :
  ∀ {l₁ : List α} (hl : l₁.length ≤ tail✝¹.length),
    (∀ (x : Nat) (hx : x < l₁.length), l₁[x] = tail✝¹[x]) → l₁ <+: tail✝¹
head✝ : α
tail✝ : List α
hl✝ : (head✝ :: tail✝).length ≤ (head✝¹ :: tail✝¹).length
h : ∀ (x : Nat) (hx : x < tail✝.length + 1), (head✝ :: tail✝)[x] = (head✝¹ :: tail✝¹)[x]
hl : tail✝.length ≤ tail✝¹.length
⊢ head✝ = head✝¹ ∧ tail✝ <+: tail✝¹

Tactic:
exact ⟨h 0 (zero_lt_succ _), tail_ih hl fun a ha ↦ h a.succ (succ_lt_succ ha)⟩

Result:
no goals