-- 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:
α : 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

Tactic:
exact w.1.symm

Result:
no goals

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 : (b :: l').length + j = l.length
h' : j < l.length
⊢ l[j] = b

Tactic:
rw [drop_eq_getElem_cons h'] 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' = l[j] :: drop (j + 1) l
⊢ l[j] = b

Proof state:
case isTrue.cons.isFalse.w
α : 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' = drop (j + 1) l

Tactic:
rw [drop_add_one_eq_tail_drop, ← w, tail_cons]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h' : ¬j < l.toArray.size
w : [] = drop j l
h : [].length + j = l.length
⊢ none =
    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:
simp

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 (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 only [getElem_toArray, this]

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
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) ⋯

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
⊢ (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:
simp at h h'

Result:
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) ⋯

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) =
    findFinIdx?.go (fun x => x == a) l l' j h

Tactic:
unfold findFinIdx?.go

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) =
    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.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) ⋯

Tactic:
rw [idxAuxOf_toArray]

Result:
case isTrue.cons.isFalse.w
α : 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' = drop (j + 1) l

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 : (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) ⋯

Tactic:
simp only [length_cons] at h

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
⊢ l.toArray.idxOfAux a (j + 1) = findFinIdx?.go (fun x => x == a) l l' (j + 1) ⋯

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
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) ⋯

Tactic:
subst this

Result:
case isFalse
α : Type u_1
inst✝ : BEq α
a : α
l : List α
j : Nat
h' : ¬j < l.toArray.size
w : [] = drop j l
h : [].length + j = l.length
⊢ none =
    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) ⋯

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
⊢ (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:
have : l[j] = b := by
  rw [drop_eq_getElem_cons h'] at w
  simp only [cons.injEq] at w
  exact w.1.symm

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
this : l[j] = b
⊢ (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) ⋯