-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) :
    l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂

Proof state:
case isFalse.cons
α : Type u_1
inst✝ : BEq α
a : α
l₁ : List α
ih : ∀ (l₂ : List α), ¬l₁.toArray.size ≤ l₂.toArray.size → l₁.isPrefixOf l₂ = false
l₂ : List α
h : ¬(a :: l₁).toArray.size ≤ l₂.toArray.size
⊢ (a :: l₁).isPrefixOf l₂ = false

Tactic:
cases l₂ with
| nil => simp
| cons b l₂ =>
  simp only [isPrefixOf_cons₂, Bool.and_eq_false_imp]
  intro w
  rw [ih]
  simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
⊢ (if h : l₁.toArray.size ≤ l₂.toArray.size then l₁.toArray.isPrefixOfAux l₂.toArray h 0 else false) = l₁.isPrefixOf l₂

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
h : l₁.toArray.size ≤ l₂.toArray.size
⊢ l₁.toArray.isPrefixOfAux l₂.toArray h 0 = l₁.isPrefixOf l₂

case isFalse
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
h : ¬l₁.toArray.size ≤ l₂.toArray.size
⊢ false = l₁.isPrefixOf l₂

Proof state:
case isFalse.cons.cons
α : Type u_1
inst✝ : BEq α
a : α
l₁ : List α
ih : ∀ (l₂ : List α), ¬l₁.toArray.size ≤ l₂.toArray.size → l₁.isPrefixOf l₂ = false
b : α
l₂ : List α
h : ¬(a :: l₁).toArray.size ≤ (b :: l₂).toArray.size
w : (a == b) = true
⊢ l₁.isPrefixOf l₂ = false

Tactic:
rw [ih]

Result:
case isFalse.cons.cons.h
α : Type u_1
inst✝ : BEq α
a : α
l₁ : List α
ih : ∀ (l₂ : List α), ¬l₁.toArray.size ≤ l₂.toArray.size → l₁.isPrefixOf l₂ = false
b : α
l₂ : List α
h : ¬(a :: l₁).toArray.size ≤ (b :: l₂).toArray.size
w : (a == b) = true
⊢ ¬l₁.toArray.size ≤ l₂.toArray.size

Proof state:
case isFalse
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
h : ¬l₁.toArray.size ≤ l₂.toArray.size
⊢ l₁.isPrefixOf l₂ = false

Tactic:
induction l₁ generalizing l₂ with
| nil => simp at h
| cons a l₁ ih =>
  cases l₂ with
  | nil => simp
  | cons b l₂ =>
    simp only [isPrefixOf_cons₂, Bool.and_eq_false_imp]
    intro w
    rw [ih]
    simp_all

Result:
no goals

Proof state:
case isFalse.cons.cons.h
α : Type u_1
inst✝ : BEq α
a : α
l₁ : List α
ih : ∀ (l₂ : List α), ¬l₁.toArray.size ≤ l₂.toArray.size → l₁.isPrefixOf l₂ = false
b : α
l₂ : List α
h : ¬(a :: l₁).toArray.size ≤ (b :: l₂).toArray.size
w : (a == b) = true
⊢ ¬l₁.toArray.size ≤ l₂.toArray.size

Tactic:
simp_all

Result:
no goals

Proof state:
case isFalse.cons.cons
α : Type u_1
inst✝ : BEq α
a : α
l₁ : List α
ih : ∀ (l₂ : List α), ¬l₁.toArray.size ≤ l₂.toArray.size → l₁.isPrefixOf l₂ = false
b : α
l₂ : List α
h : ¬(a :: l₁).toArray.size ≤ (b :: l₂).toArray.size
⊢ (a :: l₁).isPrefixOf (b :: l₂) = false

Tactic:
simp only [isPrefixOf_cons₂, Bool.and_eq_false_imp]

Result:
case isFalse.cons.cons
α : Type u_1
inst✝ : BEq α
a : α
l₁ : List α
ih : ∀ (l₂ : List α), ¬l₁.toArray.size ≤ l₂.toArray.size → l₁.isPrefixOf l₂ = false
b : α
l₂ : List α
h : ¬(a :: l₁).toArray.size ≤ (b :: l₂).toArray.size
⊢ (a == b) = true → l₁.isPrefixOf l₂ = false

Proof state:
case isFalse.cons.cons
α : Type u_1
inst✝ : BEq α
a : α
l₁ : List α
ih : ∀ (l₂ : List α), ¬l₁.toArray.size ≤ l₂.toArray.size → l₁.isPrefixOf l₂ = false
b : α
l₂ : List α
h : ¬(a :: l₁).toArray.size ≤ (b :: l₂).toArray.size
⊢ (a == b) = true → l₁.isPrefixOf l₂ = false

Tactic:
intro w

Result:
case isFalse.cons.cons
α : Type u_1
inst✝ : BEq α
a : α
l₁ : List α
ih : ∀ (l₂ : List α), ¬l₁.toArray.size ≤ l₂.toArray.size → l₁.isPrefixOf l₂ = false
b : α
l₂ : List α
h : ¬(a :: l₁).toArray.size ≤ (b :: l₂).toArray.size
w : (a == b) = true
⊢ l₁.isPrefixOf l₂ = false

Proof state:
case isFalse
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
h : ¬l₁.toArray.size ≤ l₂.toArray.size
⊢ false = l₁.isPrefixOf l₂

Tactic:
simp only [Bool.false_eq]

Result:
case isFalse
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
h : ¬l₁.toArray.size ≤ l₂.toArray.size
⊢ l₁.isPrefixOf l₂ = false

Proof state:
case isFalse.nil
α : Type u_1
inst✝ : BEq α
l₂ : List α
h : ¬#[].size ≤ l₂.toArray.size
⊢ [].isPrefixOf l₂ = false

Tactic:
simp at h

Result:
no goals

Proof state:
case isTrue
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
h : l₁.toArray.size ≤ l₂.toArray.size
⊢ l₁.toArray.isPrefixOfAux l₂.toArray h 0 = l₁.isPrefixOf l₂

Tactic:
simp [isPrefixOfAux_toArray_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
⊢ l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂

Tactic:
rw [Array.isPrefixOf]

Result:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
⊢ (if h : l₁.toArray.size ≤ l₂.toArray.size then l₁.toArray.isPrefixOfAux l₂.toArray h 0 else false) = l₁.isPrefixOf l₂

Proof state:
case isFalse.cons.nil
α : Type u_1
inst✝ : BEq α
a : α
l₁ : List α
ih : ∀ (l₂ : List α), ¬l₁.toArray.size ≤ l₂.toArray.size → l₁.isPrefixOf l₂ = false
h : ¬(a :: l₁).toArray.size ≤ #[].size
⊢ (a :: l₁).isPrefixOf [] = false

Tactic:
simp

Result:
no goals