-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Find.lean
theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) {i : Nat}
    (h : xs.findIdx? p = some i) : ∃ j, j ≤ i ∧ xs.findIdx? q = some j

Proof state:
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
i : Nat
h :
  ∃ l₁ a b, (∃ x, xs.zipIdx = l₁ ++ (a, b) :: x) ∧ (p a = true ∧ b = i) ∧ ∀ (a : α) (b : Nat), (a, b) ∈ l₁ → p a = false
⊢ ∃ j, j ≤ i ∧ findIdx? q xs = some j

Tactic:
obtain ⟨h, h₁, b, ⟨es, h₂⟩, ⟨hb, rfl⟩, h₃⟩ := h

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
h : List (α × Nat)
h₁ : α
b : Nat
es : List (α × Nat)
h₂ : xs.zipIdx = h ++ (h₁, b) :: es
h₃ : ∀ (a : α) (b : Nat), (a, b) ∈ h → p a = false
hb : p h₁ = true
⊢ ∃ j, j ≤ b ∧ findIdx? q xs = some j

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
p q : α → Bool
h₁ : α
b : Nat
hb : p h₁ = true
l₁' : List α
h₃ : ∀ (a : α) (b : Nat), (a, b) ∈ l₁'.zipIdx → p a = false
a : α
as : List α
w : ∀ (x : α), x ∈ l₁' ++ a :: as → p x = true → q x = true
h₂ : (h₁, b) = (a, 0 + l₁'.length)
⊢ ∃ j, j ≤ b ∧ findIdx? q (l₁' ++ a :: as) = some j

Tactic:
simp only [Nat.zero_add, Prod.mk.injEq] at h₂

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
p q : α → Bool
h₁ : α
b : Nat
hb : p h₁ = true
l₁' : List α
h₃ : ∀ (a : α) (b : Nat), (a, b) ∈ l₁'.zipIdx → p a = false
a : α
as : List α
w : ∀ (x : α), x ∈ l₁' ++ a :: as → p x = true → q x = true
h₂ : h₁ = a ∧ b = l₁'.length
⊢ ∃ j, j ≤ b ∧ findIdx? q (l₁' ++ a :: as) = some j

Proof state:
α : Type u_1
p q : α → Bool
h₁ : α
hb : p h₁ = true
l₁' : List α
h₃ : ∀ (a : α) (b : Nat), (a, b) ∈ l₁'.zipIdx → p a = false
as : List α
w : ∀ (x : α), x ∈ l₁' ++ h₁ :: as → p x = true → q x = true
h : findIdx? q l₁' = none
⊢ l₁'.length ≤ l₁'.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
i : Nat
h : findSome? (fun x => if p x.fst = true then some x.snd else none) xs.zipIdx = some i
⊢ ∃ j, j ≤ i ∧ findIdx? q xs = some j

Tactic:
rw [findSome?_eq_some_iff] at h

Result:
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
i : Nat
h :
  ∃ l₁ a l₂,
    xs.zipIdx = l₁ ++ a :: l₂ ∧
      (if p a.fst = true then some a.snd else none) = some i ∧
        ∀ (x : α × Nat), x ∈ l₁ → (if p x.fst = true then some x.snd else none) = none
⊢ ∃ j, j ≤ i ∧ findIdx? q xs = some j

Proof state:
α : Type u_1
p q : α → Bool
h₁ : α
hb : p h₁ = true
l₁' : List α
h₃ : ∀ (a : α) (b : Nat), (a, b) ∈ l₁'.zipIdx → p a = false
as : List α
w : ∀ (x : α), x ∈ l₁' ++ h₁ :: as → p x = true → q x = true
j : Nat
h : findIdx? q l₁' = some j
⊢ (some j).or (Option.map (fun i => i + l₁'.length) (findIdx? q (h₁ :: as))) = some j

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
i : Nat
h :
  ∃ l₁ a l₂,
    xs.zipIdx = l₁ ++ a :: l₂ ∧
      (if p a.fst = true then some a.snd else none) = some i ∧
        ∀ (x : α × Nat), x ∈ l₁ → (if p x.fst = true then some x.snd else none) = none
⊢ ∃ j, j ≤ i ∧ findIdx? q xs = some j

Tactic:
simp only [Option.ite_none_right_eq_some, Option.some.injEq, ite_eq_right_iff, reduceCtorEq,
  imp_false, Bool.not_eq_true, Prod.forall, exists_and_right, Prod.exists] at h

Result:
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
i : Nat
h :
  ∃ l₁ a b, (∃ x, xs.zipIdx = l₁ ++ (a, b) :: x) ∧ (p a = true ∧ b = i) ∧ ∀ (a : α) (b : Nat), (a, b) ∈ l₁ → p a = false
⊢ ∃ j, j ≤ i ∧ findIdx? q xs = some j

Proof state:
α : Type u_1
p q : α → Bool
h₁ : α
hb : p h₁ = true
l₁' : List α
h₃ : ∀ (a : α) (b : Nat), (a, b) ∈ l₁'.zipIdx → p a = false
as : List α
w : ∀ (x : α), x ∈ l₁' ++ h₁ :: as → p x = true → q x = true
h : findIdx? q l₁' = none
⊢ none.or (Option.map (fun i => i + l₁'.length) (findIdx? q (h₁ :: as))) = some l₁'.length

Tactic:
simp_all

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
h : List (α × Nat)
h₁ : α
b : Nat
es : List (α × Nat)
h₂ : xs.zipIdx = h ++ (h₁, b) :: es
h₃ : ∀ (a : α) (b : Nat), (a, b) ∈ h → p a = false
hb : p h₁ = true
⊢ ∃ j, j ≤ b ∧ findIdx? q xs = some j

Tactic:
rw [zipIdx_eq_append_iff] at h₂

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
h : List (α × Nat)
h₁ : α
b : Nat
es : List (α × Nat)
h₂ : ∃ l₁' l₂', xs = l₁' ++ l₂' ∧ h = l₁'.zipIdx ∧ (h₁, b) :: es = l₂'.zipIdx (0 + l₁'.length)
h₃ : ∀ (a : α) (b : Nat), (a, b) ∈ h → p a = false
hb : p h₁ = true
⊢ ∃ j, j ≤ b ∧ findIdx? q xs = some j