-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_append (p : α → Bool) (l₁ l₂ : List α) :
    (l₁ ++ l₂).findIdx p =
      if l₁.findIdx p < l₁.length then l₁.findIdx p else l₂.findIdx p + l₁.length

Proof state:
case nil
α : Type u_1
p : α → Bool
l₂ : List α
⊢ findIdx p ([] ++ l₂) = if findIdx p [] < [].length then findIdx p [] else findIdx p l₂ + [].length

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : findIdx p (xs ++ l₂) = if findIdx p xs < xs.length then findIdx p xs else findIdx p l₂ + xs.length
⊢ findIdx p (x :: xs ++ l₂) =
    if findIdx p (x :: xs) < (x :: xs).length then findIdx p (x :: xs) else findIdx p l₂ + (x :: xs).length

Tactic:
simp only [findIdx_cons, length_cons, cons_append]

Result:
case cons
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : findIdx p (xs ++ l₂) = if findIdx p xs < xs.length then findIdx p xs else findIdx p l₂ + xs.length
⊢ (bif p x then 0 else findIdx p (xs ++ l₂) + 1) =
    if (bif p x then 0 else findIdx p xs + 1) < xs.length + 1 then bif p x then 0 else findIdx p xs + 1
    else findIdx p l₂ + (xs.length + 1)

Proof state:
case cons
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : findIdx p (xs ++ l₂) = if findIdx p xs < xs.length then findIdx p xs else findIdx p l₂ + xs.length
⊢ (bif p x then 0 else findIdx p (xs ++ l₂) + 1) =
    if (bif p x then 0 else findIdx p xs + 1) < xs.length + 1 then bif p x then 0 else findIdx p xs + 1
    else findIdx p l₂ + (xs.length + 1)

Tactic:
by_cases h : p x

Result:
case pos
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : findIdx p (xs ++ l₂) = if findIdx p xs < xs.length then findIdx p xs else findIdx p l₂ + xs.length
h : p x = true
⊢ (bif p x then 0 else findIdx p (xs ++ l₂) + 1) =
    if (bif p x then 0 else findIdx p xs + 1) < xs.length + 1 then bif p x then 0 else findIdx p xs + 1
    else findIdx p l₂ + (xs.length + 1)

case neg
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : findIdx p (xs ++ l₂) = if findIdx p xs < xs.length then findIdx p xs else findIdx p l₂ + xs.length
h : ¬p x = true
⊢ (bif p x then 0 else findIdx p (xs ++ l₂) + 1) =
    if (bif p x then 0 else findIdx p xs + 1) < xs.length + 1 then bif p x then 0 else findIdx p xs + 1
    else findIdx p l₂ + (xs.length + 1)

Proof state:
case neg
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : findIdx p (xs ++ l₂) = if findIdx p xs < xs.length then findIdx p xs else findIdx p l₂ + xs.length
h : ¬p x = true
⊢ (if findIdx p xs < xs.length then findIdx p xs else findIdx p l₂ + xs.length) + 1 =
    if findIdx p xs < xs.length then findIdx p xs + 1 else findIdx p l₂ + (xs.length + 1)

Tactic:
split <;> simp [Nat.add_assoc]

Result:
no goals

Proof state:
case pos
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : findIdx p (xs ++ l₂) = if findIdx p xs < xs.length then findIdx p xs else findIdx p l₂ + xs.length
h : p x = true
⊢ (bif p x then 0 else findIdx p (xs ++ l₂) + 1) =
    if (bif p x then 0 else findIdx p xs + 1) < xs.length + 1 then bif p x then 0 else findIdx p xs + 1
    else findIdx p l₂ + (xs.length + 1)

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : findIdx p (xs ++ l₂) = if findIdx p xs < xs.length then findIdx p xs else findIdx p l₂ + xs.length
h : ¬p x = true
⊢ (bif p x then 0 else findIdx p (xs ++ l₂) + 1) =
    if (bif p x then 0 else findIdx p xs + 1) < xs.length + 1 then bif p x then 0 else findIdx p xs + 1
    else findIdx p l₂ + (xs.length + 1)

Tactic:
simp only [h, ih, cond_eq_if, Bool.false_eq_true, ↓reduceIte, add_one_lt_add_one_iff]

Result:
case neg
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : findIdx p (xs ++ l₂) = if findIdx p xs < xs.length then findIdx p xs else findIdx p l₂ + xs.length
h : ¬p x = true
⊢ (if findIdx p xs < xs.length then findIdx p xs else findIdx p l₂ + xs.length) + 1 =
    if findIdx p xs < xs.length then findIdx p xs + 1 else findIdx p l₂ + (xs.length + 1)