-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem takeWhile_eq_takeWhileTR : @takeWhile = @takeWhileTR

Proof state:
case h.h.h.cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs
acc : Array α
⊢ l = acc.toList ++ x :: xs → takeWhileTR.go p l (x :: xs) acc = acc.toList ++ takeWhile p (x :: xs)

Tactic:
simp only [takeWhileTR.go, Array.toListImpl_eq, takeWhile]

Result:
case h.h.h.cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs
acc : Array α
⊢ l = acc.toList ++ x :: xs →
    (bif p x then takeWhileTR.go p l xs (acc.push x) else acc.toList) =
      acc.toList ++
        match p x with
        | true => x :: takeWhile p xs
        | false => []

Proof state:
case h.h.h.cons.h_2
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = false
⊢ l = acc.toList ++ x :: xs → (bif p x then takeWhileTR.go p l xs (acc.push x) else acc.toList) = acc.toList ++ []

Tactic:
simp [*]

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs

Tactic:
intro xs

Result:
case h.h.h
α : Type u_1
p : α → Bool
l xs : List α
⊢ ∀ (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs

Proof state:
case h.h.h.cons.h_1
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.toList ++ x :: xs
⊢ (bif p x then takeWhileTR.go p l xs (acc.push x) else acc.toList) = acc.toList ++ x :: takeWhile p xs

Tactic:
rw [IH] <;> simp_all

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = takeWhileTR.go p l l #[]

Tactic:
suffices ∀ xs acc, l = acc.toList ++ xs →
    takeWhileTR.go p l xs acc = acc.toList ++ xs.takeWhile p from
  (this l #[] (by simp)).symm

Result:
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs

Proof state:
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = takeWhileTR p l

Tactic:
simp [takeWhileTR]

Result:
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = takeWhileTR.go p l l #[]

Proof state:
α : Type u_1
p : α → Bool
l : List α
this : ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs
⊢ l = #[].toList ++ l

Tactic:
simp

Result:
no goals

Proof state:
⊢ @takeWhile = @takeWhileTR

Tactic:
funext α p l

Result:
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = takeWhileTR p l

Proof state:
case h.h.h.nil
α : Type u_1
p : α → Bool
l : List α
acc : Array α
⊢ l = acc.toList ++ [] → takeWhileTR.go p l [] acc = acc.toList ++ takeWhile p []

Tactic:
simp [takeWhile, takeWhileTR.go]

Result:
no goals

Proof state:
case h.h.h.cons.h_1
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
⊢ l = acc.toList ++ x :: xs →
    (bif p x then takeWhileTR.go p l xs (acc.push x) else acc.toList) = acc.toList ++ x :: takeWhile p xs

Tactic:
intro h

Result:
case h.h.h.cons.h_1
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.toList ++ x :: xs
⊢ (bif p x then takeWhileTR.go p l xs (acc.push x) else acc.toList) = acc.toList ++ x :: takeWhile p xs

Proof state:
case h.h.h.cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs
acc : Array α
⊢ l = acc.toList ++ x :: xs →
    (bif p x then takeWhileTR.go p l xs (acc.push x) else acc.toList) =
      acc.toList ++
        match p x with
        | true => x :: takeWhile p xs
        | false => []

Tactic:
split

Result:
case h.h.h.cons.h_1
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
⊢ l = acc.toList ++ x :: xs →
    (bif p x then takeWhileTR.go p l xs (acc.push x) else acc.toList) = acc.toList ++ x :: takeWhile p xs

case h.h.h.cons.h_2
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → takeWhileTR.go p l xs acc = acc.toList ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = false
⊢ l = acc.toList ++ x :: xs → (bif p x then takeWhileTR.go p l xs (acc.push x) else acc.toList) = acc.toList ++ []