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

Tactic:
obtain ⟨rfl, rfl⟩ := h₂

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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, j ≤ l₁'.length ∧ findIdx? q (l₁' ++ h₁ :: as) = some j

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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, j ≤ l₁'.length ∧ findIdx? q (l₁' ++ h₁ :: as) = some j

Tactic:
simp only [findIdx?_append]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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, j ≤ l₁'.length ∧ (findIdx? q l₁').or (Option.map (fun i => i + l₁'.length) (findIdx? q (h₁ :: as))) = 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 : findIdx? p xs = some i
⊢ ∃ j, j ≤ i ∧ findIdx? q xs = some j

Tactic:
simp only [findIdx?_eq_findSome?_zipIdx] at h

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

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

Tactic:
obtain ⟨a, as, rfl, h₂, rfl⟩ := 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₁, b) = (a, 0 + l₁'.length)
⊢ ∃ j, j ≤ b ∧ findIdx? q (l₁' ++ a :: as) = some j

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

Tactic:
rw [eq_comm, zipIdx_eq_cons_iff] at h₂

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
p q : α → Bool
h₁ : α
b : Nat
es : List (α × Nat)
hb : p h₁ = true
l₁' l₂' : List α
w : ∀ (x : α), x ∈ l₁' ++ l₂' → p x = true → q x = true
h₂ : ∃ a as, l₂' = a :: as ∧ (h₁, b) = (a, 0 + l₁'.length) ∧ es = as.zipIdx (0 + l₁'.length + 1)
h₃ : ∀ (a : α) (b : Nat), (a, b) ∈ l₁'.zipIdx → p a = false
⊢ ∃ j, j ≤ b ∧ findIdx? q (l₁' ++ l₂') = 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
⊢ ∃ j_1, j_1 ≤ l₁'.length ∧ (some j).or (Option.map (fun i => i + l₁'.length) (findIdx? q (h₁ :: as))) = some j_1

Tactic:
refine ⟨j, ?_, by simp⟩

Result:
α : 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
⊢ j ≤ l₁'.length

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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, j ≤ l₁'.length ∧ (findIdx? q l₁').or (Option.map (fun i => i + l₁'.length) (findIdx? q (h₁ :: as))) = some j

Tactic:
match h : findIdx? q l₁' with
| some j =>
  refine ⟨j, ?_, by simp⟩
  rw [findIdx?_eq_some_iff_findIdx_eq] at h
  omega
| none =>
  refine ⟨l₁'.length, by simp, by simp_all⟩

Result:
no goals

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 : j < l₁'.length ∧ findIdx q l₁' = j
⊢ j ≤ l₁'.length

Tactic:
omega

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₂ : ∃ 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

Tactic:
obtain ⟨l₁', l₂', rfl, rfl, h₂⟩ := h₂

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
p q : α → Bool
h₁ : α
b : Nat
es : List (α × Nat)
hb : p h₁ = true
l₁' l₂' : List α
w : ∀ (x : α), x ∈ l₁' ++ l₂' → p x = true → q x = true
h₂ : (h₁, b) :: es = l₂'.zipIdx (0 + l₁'.length)
h₃ : ∀ (a : α) (b : Nat), (a, b) ∈ l₁'.zipIdx → p a = false
⊢ ∃ j, j ≤ b ∧ findIdx? q (l₁' ++ l₂') = 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
⊢ ∃ j, j ≤ l₁'.length ∧ none.or (Option.map (fun i => i + l₁'.length) (findIdx? q (h₁ :: as))) = some j

Tactic:
refine ⟨l₁'.length, by simp, by simp_all⟩

Result:
no goals

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
⊢ j ≤ l₁'.length

Tactic:
rw [findIdx?_eq_some_iff_findIdx_eq] at h

Result:
α : 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 : j < l₁'.length ∧ findIdx q l₁' = j
⊢ j ≤ l₁'.length