-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = some l₁[i]

Proof state:
case cons.nil
α✝ : Type u_1
a : α✝
l₁ : List α✝
ih : ∀ {l₂ : List α✝}, l₁ <+: l₂ ↔ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]
⊢ a :: l₁ <+: [] ↔ ∀ (i : Nat) (h : i < (a :: l₁).length), [][i]? = some (a :: l₁)[i]

Tactic:
simpa using ⟨0, by simp⟩

Result:
no goals

Proof state:
case cons.cons
α✝ : Type u_1
a : α✝
l₁ : List α✝
ih : ∀ {l₂ : List α✝}, l₁ <+: l₂ ↔ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]
b : α✝
l₂ : List α✝
⊢ (a = b ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]) ↔
    (∀ (h : 0 < (a :: l₁).length), (b :: l₂)[0]? = some (a :: l₁)[0]) ∧
      ∀ (n : Nat) (h : n + 1 < (a :: l₁).length), (b :: l₂)[n + 1]? = some (a :: l₁)[n + 1]

Tactic:
simp [Nat.succ_lt_succ_iff, eq_comm]

Result:
no goals

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁ <+: l₂ ↔ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]

Tactic:
induction l₁ generalizing l₂ with
| nil => simp
| cons a l₁ ih =>
  cases l₂ with
  | nil =>
    simpa using ⟨0, by simp⟩
  | cons b l₂ =>
    simp only [cons_append, cons_prefix_cons, ih]
    rw (occs := [2]) [← Nat.and_forall_add_one]
    simp [Nat.succ_lt_succ_iff, eq_comm]

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
a : α✝
l₁ : List α✝
ih : ∀ {l₂ : List α✝}, l₁ <+: l₂ ↔ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]
l₂ : List α✝
⊢ a :: l₁ <+: l₂ ↔ ∀ (i : Nat) (h : i < (a :: l₁).length), l₂[i]? = some (a :: l₁)[i]

Tactic:
cases l₂ with
| nil =>
  simpa using ⟨0, by simp⟩
| cons b l₂ =>
  simp only [cons_append, cons_prefix_cons, ih]
  rw (occs := [2]) [← Nat.and_forall_add_one]
  simp [Nat.succ_lt_succ_iff, eq_comm]

Result:
no goals

Proof state:
case nil
α✝ : Type u_1
l₂ : List α✝
⊢ [] <+: l₂ ↔ ∀ (i : Nat) (h : i < [].length), l₂[i]? = some [][i]

Tactic:
simp

Result:
no goals

Proof state:
α✝ : Type u_1
a : α✝
l₁ : List α✝
ih : ∀ {l₂ : List α✝}, l₁ <+: l₂ ↔ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]
⊢ 0 < l₁.length + 1

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
α✝ : Type u_1
a : α✝
l₁ : List α✝
ih : ∀ {l₂ : List α✝}, l₁ <+: l₂ ↔ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]
b : α✝
l₂ : List α✝
⊢ a :: l₁ <+: b :: l₂ ↔ ∀ (i : Nat) (h : i < (a :: l₁).length), (b :: l₂)[i]? = some (a :: l₁)[i]

Tactic:
simp only [cons_append, cons_prefix_cons, ih]

Result:
case cons.cons
α✝ : Type u_1
a : α✝
l₁ : List α✝
ih : ∀ {l₂ : List α✝}, l₁ <+: l₂ ↔ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]
b : α✝
l₂ : List α✝
⊢ (a = b ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]) ↔
    ∀ (i : Nat) (h : i < (a :: l₁).length), (b :: l₂)[i]? = some (a :: l₁)[i]

Proof state:
case cons.cons
α✝ : Type u_1
a : α✝
l₁ : List α✝
ih : ∀ {l₂ : List α✝}, l₁ <+: l₂ ↔ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]
b : α✝
l₂ : List α✝
⊢ (a = b ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]) ↔
    ∀ (i : Nat) (h : i < (a :: l₁).length), (b :: l₂)[i]? = some (a :: l₁)[i]

Tactic:
rw (occs := [2]) [← Nat.and_forall_add_one]

Result:
case cons.cons
α✝ : Type u_1
a : α✝
l₁ : List α✝
ih : ∀ {l₂ : List α✝}, l₁ <+: l₂ ↔ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]
b : α✝
l₂ : List α✝
⊢ (a = b ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]) ↔
    (∀ (h : 0 < (a :: l₁).length), (b :: l₂)[0]? = some (a :: l₁)[0]) ∧
      ∀ (n : Nat) (h : n + 1 < (a :: l₁).length), (b :: l₂)[n + 1]? = some (a :: l₁)[n + 1]