-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
    Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
      Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ (if h : i + 1 < l₁.toArray.size then
      let a := l₁.toArray[i + 1];
      let_fun this := ⋯;
      let b := l₂.toArray[i + 1];
      if (a == b) = true then l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1 + 1) else false
    else true) =
    l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ i

Tactic:
conv => rhs; rw [Array.isPrefixOfAux]

Result:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ (if h : i + 1 < l₁.toArray.size then
      let a := l₁.toArray[i + 1];
      let_fun this := ⋯;
      let b := l₂.toArray[i + 1];
      if (a == b) = true then l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1 + 1) else false
    else true) =
    if h : i < l₁.tail.toArray.size then
      let a := l₁.tail.toArray[i];
      let_fun this := ⋯;
      let b := l₂.tail.toArray[i];
      if (a == b) = true then l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ (i + 1) else false
    else true

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ (if h : i + 1 < l₁.length then
      decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1 + 1)
    else true) =
    if h : i < l₁.length - 1 then
      decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ (i + 1)
    else true

Tactic:
split <;> rename_i h₁ <;> split <;> rename_i h₂

Result:
case isTrue.isTrue
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
h₁ : i + 1 < l₁.length
h₂ : i < l₁.length - 1
⊢ (decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1 + 1)) =
    (decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ (i + 1))

case isTrue.isFalse
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
h₁ : i + 1 < l₁.length
h₂ : ¬i < l₁.length - 1
⊢ (decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1 + 1)) = true

case isFalse.isTrue
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
h₁ : ¬i + 1 < l₁.length
h₂ : i < l₁.length - 1
⊢ true = (decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ (i + 1))

case isFalse.isFalse
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
h₁ : ¬i + 1 < l₁.length
h₂ : ¬i < l₁.length - 1
⊢ true = true

Proof state:
case isTrue.isTrue
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
h₁ : i + 1 < l₁.length
h₂ : i < l₁.length - 1
⊢ (decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1 + 1)) =
    (decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ (i + 1))

Tactic:
rw [isPrefixOfAux_toArray_succ]

Result:
no goals

Proof state:
case isFalse.isTrue
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
h₁ : ¬i + 1 < l₁.length
h₂ : i < l₁.length - 1
⊢ true = (decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ (i + 1))

Tactic:
omega

Result:
no goals

Proof state:
case isFalse.isFalse
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
h₁ : ¬i + 1 < l₁.length
h₂ : ¬i < l₁.length - 1
⊢ true = true

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1) = l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ i

Tactic:
rw [Array.isPrefixOfAux]

Result:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ (if h : i + 1 < l₁.toArray.size then
      let a := l₁.toArray[i + 1];
      let_fun this := ⋯;
      let b := l₂.toArray[i + 1];
      if (a == b) = true then l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1 + 1) else false
    else true) =
    l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ i

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ (if h : i + 1 < l₁.toArray.size then
      let a := l₁.toArray[i + 1];
      let_fun this := ⋯;
      let b := l₂.toArray[i + 1];
      if (a == b) = true then l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1 + 1) else false
    else true) =
    if h : i < l₁.tail.toArray.size then
      let a := l₁.tail.toArray[i];
      let_fun this := ⋯;
      let b := l₂.tail.toArray[i];
      if (a == b) = true then l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ (i + 1) else false
    else true

Tactic:
simp only [size_toArray, getElem_toArray, Bool.if_false_right, length_tail, getElem_tail]

Result:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ (if h : i + 1 < l₁.length then
      decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1 + 1)
    else true) =
    if h : i < l₁.length - 1 then
      decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ (i + 1)
    else true

Proof state:
α : Type ?u.60176
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ l₁.tail.toArray.size ≤ l₂.tail.toArray.size

Tactic:
simp

Result:
α : Type ?u.60176
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ l₁.length - 1 ≤ l₂.length - 1

Proof state:
α : Type ?u.60176
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ l₁.length - 1 ≤ l₂.length - 1

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.isFalse
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
h₁ : i + 1 < l₁.length
h₂ : ¬i < l₁.length - 1
⊢ (decide ((l₁[i + 1] == l₂[i + 1]) = true) && l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1 + 1)) = true

Tactic:
omega

Result:
no goals