-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_le_findIdx {l : List α} {p q : α → Bool} (h : ∀ x ∈ l, p x → q x) : l.findIdx q ≤ l.findIdx p

Proof state:
case cons.isFalse.isFalse
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
h✝¹ : ¬q x = true
h✝ : ¬p x = true
⊢ findIdx q xs + 1 ≤ findIdx p xs + 1

Tactic:
simp only [Nat.add_le_add_iff_right]

Result:
case cons.isFalse.isFalse
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
h✝¹ : ¬q x = true
h✝ : ¬p x = true
⊢ findIdx q xs ≤ findIdx p xs

Proof state:
case cons.isFalse.isTrue
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
h✝¹ : ¬q x = true
h✝ : p x = true
⊢ findIdx q xs + 1 ≤ 0

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.isFalse.isFalse
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
h✝¹ : ¬q x = true
h✝ : ¬p x = true
⊢ findIdx q xs ≤ findIdx p xs

Tactic:
exact ih fun _ m w => h _ (mem_cons_of_mem x m) w

Result:
no goals

Proof state:
case nil
α : Type u_1
p q : α → Bool
h : ∀ (x : α), x ∈ [] → p x = true → q x = true
⊢ findIdx q [] ≤ findIdx p []

Tactic:
simp

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
h✝ : ¬q x = true
⊢ findIdx q xs + 1 ≤ if p x = true then 0 else findIdx p xs + 1

Tactic:
split

Result:
case cons.isFalse.isTrue
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
h✝¹ : ¬q x = true
h✝ : p x = true
⊢ findIdx q xs + 1 ≤ 0

case cons.isFalse.isFalse
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
h✝¹ : ¬q x = true
h✝ : ¬p x = true
⊢ findIdx q xs + 1 ≤ findIdx p xs + 1

Proof state:
case cons.isTrue
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
h✝ : q x = true
⊢ 0 ≤ if p x = true then 0 else findIdx p xs + 1

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
⊢ (if q x = true then 0 else findIdx q xs + 1) ≤ if p x = true then 0 else findIdx p xs + 1

Tactic:
split

Result:
case cons.isTrue
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
h✝ : q x = true
⊢ 0 ≤ if p x = true then 0 else findIdx p xs + 1

case cons.isFalse
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
h✝ : ¬q x = true
⊢ findIdx q xs + 1 ≤ if p x = true then 0 else findIdx p xs + 1

Proof state:
case cons
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
⊢ findIdx q (x :: xs) ≤ findIdx p (x :: xs)

Tactic:
simp only [findIdx_cons, cond_eq_if]

Result:
case cons
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x = true → q x = true) → findIdx q xs ≤ findIdx p xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true → q x_1 = true
⊢ (if q x = true then 0 else findIdx q xs + 1) ≤ if p x = true then 0 else findIdx p xs + 1