-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem findFinIdx?_loop_toArray (w : l' = l.drop j) :
    Array.findFinIdx?.loop p l.toArray j = List.findFinIdx?.go p l l' j h

Proof state:
α✝ : Type u_1
l' : List α✝
p : α✝ → Bool
j : Nat
l : List α✝
h : l'.length + j = l.length
w : l' = drop j l
⊢ findFinIdx?.loop p l.toArray j = findFinIdx?.go p l l' j h

Tactic:
unfold findFinIdx?.loop

Result:
α✝ : Type u_1
l' : List α✝
p : α✝ → Bool
j : Nat
l : List α✝
h : l'.length + j = l.length
w : l' = drop j l
⊢ (if h : j < l.toArray.size then if p l.toArray[j] = true then some ⟨j, h⟩ else findFinIdx?.loop p l.toArray (j + 1)
    else none) =
    findFinIdx?.go p l l' j h

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

Tactic:
simp

Result:
no goals

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

α✝ : Type u_1
p : α✝ → Bool
j : Nat
l : List α✝
h' : j < l.toArray.size
a : α✝
l' : List α✝
h : (a :: l').length + j = l.length
w : a :: l' = drop j l
⊢ j < l.length

Tactic:
exact w.1.symm

Result:
no goals

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

α✝ : Type u_1
p : α✝ → Bool
j : Nat
l : List α✝
h' : j < l.toArray.size
a : α✝
l' : List α✝
h : (a :: l').length + j = l.length
w : a :: l' = drop j l
⊢ j < l.length

Tactic:
simp only [cons.injEq] at w

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

α✝ : Type u_1
p : α✝ → Bool
j : Nat
l : List α✝
h' : j < l.toArray.size
a : α✝
l' : List α✝
h : (a :: l').length + j = l.length
w : a :: l' = drop j l
⊢ j < l.length

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

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

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

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

Tactic:
have : l[j] = a := by
  rw [drop_eq_getElem_cons] at w
  simp only [cons.injEq] at w
  exact w.1.symm

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.cons.isFalse
α✝ : Type u_1
p : α✝ → Bool
j : Nat
l : List α✝
h' : j < l.toArray.size
a : α✝
l' : List α✝
h : l'.length + 1 + j = l.length
w : a :: l' = drop j l
this : l[j] = a
h✝ : ¬p a = true
⊢ findFinIdx?.loop p l.toArray (j + 1) = findFinIdx?.go p l l' (j + 1) ⋯

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

Result:
case isTrue.cons.isFalse
α✝ : Type u_1
p : α✝ → Bool
j : Nat
l : List α✝
h' : j < l.toArray.size
a : α✝
l' : List α✝
h : l'.length + 1 + j = l.length
w : a :: l' = drop j l
this✝ : l[j] = a
h✝ : ¬p a = true
this : l.length - (j + 1) < l.length - j
⊢ findFinIdx?.loop p l.toArray (j + 1) = findFinIdx?.go p l l' (j + 1) ⋯

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

Tactic:
simp only [getElem_toArray, this]

Result:
case isTrue.cons
α✝ : Type u_1
p : α✝ → Bool
j : Nat
l : List α✝
h' : j < l.toArray.size
a : α✝
l' : List α✝
h : (a :: l').length + j = l.length
w : a :: l' = drop j l
this : l[j] = a
⊢ (if p a = true then some ⟨j, h'⟩ else findFinIdx?.loop p l.toArray (j + 1)) =
    if p a = true then some ⟨j, ⋯⟩ else findFinIdx?.go p l l' (j + 1) ⋯

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

Tactic:
split <;> rename_i h'

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

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

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

Tactic:
rfl

Result:
no goals