-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem idxAuxOf_toArray [BEq α] (a : α) (l : List α) (j : Nat) (w : l' = l.drop j) (h) :
    l.toArray.idxOfAux a j = findFinIdx?.go (fun x => x == a) l l' j h

Proof state:
case isFalse
α : Type u_1
l' : List α
inst✝ : BEq α
a : α
l : List α
j : Nat
w : l' = drop j l
h : l'.length + j = l.length
h' : ¬j < l.toArray.size
⊢ none =
    match l', j, h with
    | [], x, x_1 => none
    | a_1 :: l_1, i, h => if (a_1 == a) = true then some ⟨i, ⋯⟩ else findFinIdx?.go (fun x => x == a) l l_1 (i + 1) ⋯

Tactic:
have : l' = [] := by simp_all

Result:
case isFalse
α : Type u_1
l' : List α
inst✝ : BEq α
a : α
l : List α
j : Nat
w : l' = drop j l
h : l'.length + j = l.length
h' : ¬j < l.toArray.size
this : l' = []
⊢ none =
    match l', j, h with
    | [], x, x_1 => none
    | a_1 :: l_1, i, h => if (a_1 == a) = true then some ⟨i, ⋯⟩ else findFinIdx?.go (fun x => x == a) l l_1 (i + 1) ⋯

Proof state:
case isTrue.nil
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h'✝ : j < l.toArray.size
w : [] = drop j l
h✝ : [].length + j = l.length
h : j = l.length
h' : j < l.length
⊢ (if (l.toArray[j] == a) = true then some ⟨j, h'✝⟩ else l.toArray.idxOfAux a (j + 1)) =
    match [], j, h✝ with
    | [], x, x_1 => none
    | a_1 :: l_1, i, h => if (a_1 == a) = true then some ⟨i, ⋯⟩ else findFinIdx?.go (fun x => x == a) l l_1 (i + 1) ⋯

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.cons.isTrue
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h'✝ : j < l.toArray.size
b : α
l' : List α
w : b :: l' = drop j l
h : (b :: l').length + j = l.length
h' : j < l.length
this : l[j] = b
h✝ : (b == a) = true
⊢ some ⟨j, h'✝⟩ = some ⟨j, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l' : List α
inst✝ : BEq α
a : α
l : List α
j : Nat
w : l' = drop j l
h : l'.length + j = l.length
⊢ (if h : j < l.toArray.size then if (l.toArray[j] == a) = true then some ⟨j, h⟩ else l.toArray.idxOfAux a (j + 1)
    else none) =
    match l', j, h with
    | [], x, x_1 => none
    | a_1 :: l_1, i, h => if (a_1 == a) = true then some ⟨i, ⋯⟩ else findFinIdx?.go (fun x => x == a) l l_1 (i + 1) ⋯

Tactic:
split <;> rename_i h'

Result:
case isTrue
α : Type u_1
l' : List α
inst✝ : BEq α
a : α
l : List α
j : Nat
w : l' = drop j l
h : l'.length + j = l.length
h' : j < l.toArray.size
⊢ (if (l.toArray[j] == a) = true then some ⟨j, h'⟩ else l.toArray.idxOfAux a (j + 1)) =
    match l', j, h with
    | [], x, x_1 => none
    | a_1 :: l_1, i, h => if (a_1 == a) = true then some ⟨i, ⋯⟩ else findFinIdx?.go (fun x => x == a) l l_1 (i + 1) ⋯

case isFalse
α : Type u_1
l' : List α
inst✝ : BEq α
a : α
l : List α
j : Nat
w : l' = drop j l
h : l'.length + j = l.length
h' : ¬j < l.toArray.size
⊢ none =
    match l', j, h with
    | [], x, x_1 => none
    | a_1 :: l_1, i, h => if (a_1 == a) = true then some ⟨i, ⋯⟩ else findFinIdx?.go (fun x => x == a) l l_1 (i + 1) ⋯

Proof state:
α : Type u_1
l' : List α
inst✝ : BEq α
a : α
l : List α
j : Nat
w : l' = drop j l
h : l'.length + j = l.length
h' : ¬j < l.toArray.size
⊢ l' = []

Tactic:
simp_all

Result:
no goals

Proof state:
case isTrue.cons
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h'✝ : j < l.toArray.size
b : α
l' : List α
w : b :: l' = drop j l
h : (b :: l').length + j = l.length
h' : j < l.length
this : l[j] = b
⊢ (if (b == a) = true then some ⟨j, h'✝⟩ else l.toArray.idxOfAux a (j + 1)) =
    if (b == a) = true then some ⟨j, ⋯⟩ else findFinIdx?.go (fun x => x == a) l l' (j + 1) ⋯

Tactic:
split

Result:
case isTrue.cons.isTrue
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h'✝ : j < l.toArray.size
b : α
l' : List α
w : b :: l' = drop j l
h : (b :: l').length + j = l.length
h' : j < l.length
this : l[j] = b
h✝ : (b == a) = true
⊢ some ⟨j, h'✝⟩ = some ⟨j, ⋯⟩

case isTrue.cons.isFalse
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h'✝ : j < l.toArray.size
b : α
l' : List α
w : b :: l' = drop j l
h : (b :: l').length + j = l.length
h' : j < l.length
this : l[j] = b
h✝ : ¬(b == a) = true
⊢ l.toArray.idxOfAux a (j + 1) = findFinIdx?.go (fun x => x == a) l l' (j + 1) ⋯

Proof state:
α : Type u_1
l' : List α
inst✝ : BEq α
a : α
l : List α
j : Nat
w : l' = drop j l
h : l'.length + j = l.length
⊢ l.toArray.idxOfAux a j = findFinIdx?.go (fun x => x == a) l l' j h

Tactic:
unfold idxOfAux

Result:
α : Type u_1
l' : List α
inst✝ : BEq α
a : α
l : List α
j : Nat
w : l' = drop j l
h : l'.length + j = l.length
⊢ (if h : j < l.toArray.size then if (l.toArray[j] == a) = true then some ⟨j, h⟩ else l.toArray.idxOfAux a (j + 1)
    else none) =
    findFinIdx?.go (fun x => x == a) l l' j h

Proof state:
case isTrue.cons.isFalse
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h'✝ : j < l.toArray.size
b : α
l' : List α
w : b :: l' = drop j l
h : l'.length + 1 + j = l.length
h' : j < l.length
this : l[j] = b
h✝ : ¬(b == a) = true
⊢ l.toArray.idxOfAux a (j + 1) = findFinIdx?.go (fun x => x == a) l l' (j + 1) ⋯

Tactic:
have : l.length - (j + 1) < l.length - j := by omega

Result:
case isTrue.cons.isFalse
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h'✝ : j < l.toArray.size
b : α
l' : List α
w : b :: l' = drop j l
h : l'.length + 1 + j = l.length
h' : j < l.length
this✝ : l[j] = b
h✝ : ¬(b == a) = true
this : l.length - (j + 1) < l.length - j
⊢ l.toArray.idxOfAux a (j + 1) = findFinIdx?.go (fun x => x == a) l l' (j + 1) ⋯

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h'✝ : j < l.toArray.size
b : α
l' : List α
w : b :: l' = drop j l
h : l'.length + 1 + j = l.length
h' : j < l.length
this : l[j] = b
h✝ : ¬(b == a) = true
⊢ l.length - (j + 1) < l.length - j

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.cons
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h' : j < l.toArray.size
b : α
l' : List α
w : b :: l' = drop j l
h : (b :: l').length + j = l.length
⊢ (if (l.toArray[j] == a) = true then some ⟨j, h'⟩ else l.toArray.idxOfAux a (j + 1)) =
    match b :: l', j, h with
    | [], x, x_1 => none
    | a_1 :: l_1, i, h => if (a_1 == a) = true then some ⟨i, ⋯⟩ else findFinIdx?.go (fun x => x == a) l l_1 (i + 1) ⋯

Tactic:
simp at h'

Result:
case isTrue.cons
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h'✝ : j < l.toArray.size
b : α
l' : List α
w : b :: l' = drop j l
h : (b :: l').length + j = l.length
h' : j < l.length
⊢ (if (l.toArray[j] == a) = true then some ⟨j, h'✝⟩ else l.toArray.idxOfAux a (j + 1)) =
    match b :: l', j, h with
    | [], x, x_1 => none
    | a_1 :: l_1, i, h => if (a_1 == a) = true then some ⟨i, ⋯⟩ else findFinIdx?.go (fun x => x == a) l l_1 (i + 1) ⋯

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h'✝ : j < l.toArray.size
b : α
l' : List α
h : (b :: l').length + j = l.length
h' : j < l.length
w : b :: l' = l[j] :: drop (j + 1) l
⊢ l[j] = b

Tactic:
simp only [cons.injEq] at w

Result:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h'✝ : j < l.toArray.size
b : α
l' : List α
h : (b :: l').length + j = l.length
h' : j < l.length
w : b = l[j] ∧ l' = drop (j + 1) l
⊢ l[j] = b