-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem takeWhile_append {xs ys : List α} :
    (xs ++ ys).takeWhile p =
      if (xs.takeWhile p).length = xs.length then xs ++ ys.takeWhile p else xs.takeWhile p

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
ys : List α
x : α
xs : List α
ih : takeWhile p (xs ++ ys) = if (takeWhile p xs).length = xs.length then xs ++ takeWhile p ys else takeWhile p xs
h✝ : p x = true
⊢ x :: takeWhile p (xs ++ ys) =
    if (x :: takeWhile p xs).length = (x :: xs).length then x :: (xs ++ takeWhile p ys) else x :: takeWhile p xs

Tactic:
simp_all only [length_cons, add_one_inj]

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
ys : List α
x : α
xs : List α
ih : takeWhile p (xs ++ ys) = if (takeWhile p xs).length = xs.length then xs ++ takeWhile p ys else takeWhile p xs
h✝ : p x = true
⊢ (x :: if (takeWhile p xs).length = xs.length then xs ++ takeWhile p ys else takeWhile p xs) =
    if (takeWhile p xs).length = xs.length then x :: (xs ++ takeWhile p ys) else x :: takeWhile p xs

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
ys : List α
x : α
xs : List α
ih : takeWhile p (xs ++ ys) = if (takeWhile p xs).length = xs.length then xs ++ takeWhile p ys else takeWhile p xs
h✝ : p x = true
⊢ (x :: if (takeWhile p xs).length = xs.length then xs ++ takeWhile p ys else takeWhile p xs) =
    if (takeWhile p xs).length = xs.length then x :: (xs ++ takeWhile p ys) else x :: takeWhile p xs

Tactic:
split <;> rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
ys : List α
x : α
xs : List α
ih : takeWhile p (xs ++ ys) = if (takeWhile p xs).length = xs.length then xs ++ takeWhile p ys else takeWhile p xs
⊢ (if p x = true then x :: takeWhile p (xs ++ ys) else []) =
    if (if p x = true then x :: takeWhile p xs else []).length = (x :: xs).length then x :: (xs ++ takeWhile p ys)
    else if p x = true then x :: takeWhile p xs else []

Tactic:
split

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
ys : List α
x : α
xs : List α
ih : takeWhile p (xs ++ ys) = if (takeWhile p xs).length = xs.length then xs ++ takeWhile p ys else takeWhile p xs
h✝ : p x = true
⊢ x :: takeWhile p (xs ++ ys) =
    if (x :: takeWhile p xs).length = (x :: xs).length then x :: (xs ++ takeWhile p ys) else x :: takeWhile p xs

case cons.isFalse
α : Type u_1
p : α → Bool
ys : List α
x : α
xs : List α
ih : takeWhile p (xs ++ ys) = if (takeWhile p xs).length = xs.length then xs ++ takeWhile p ys else takeWhile p xs
h✝ : ¬p x = true
⊢ [] = if [].length = (x :: xs).length then x :: (xs ++ takeWhile p ys) else []

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

Tactic:
simp

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
ys : List α
x : α
xs : List α
ih : takeWhile p (xs ++ ys) = if (takeWhile p xs).length = xs.length then xs ++ takeWhile p ys else takeWhile p xs
h✝ : ¬p x = true
⊢ [] = if [].length = (x :: xs).length then x :: (xs ++ takeWhile p ys) else []

Tactic:
simp_all

Result:
no goals

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

Tactic:
simp only [cons_append, takeWhile_cons]

Result:
case cons
α : Type u_1
p : α → Bool
ys : List α
x : α
xs : List α
ih : takeWhile p (xs ++ ys) = if (takeWhile p xs).length = xs.length then xs ++ takeWhile p ys else takeWhile p xs
⊢ (if p x = true then x :: takeWhile p (xs ++ ys) else []) =
    if (if p x = true then x :: takeWhile p xs else []).length = (x :: xs).length then x :: (xs ++ takeWhile p ys)
    else if p x = true then x :: takeWhile p xs else []