case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = takeWhileTR p l
⊢ @takeWhile = @takeWhileTR
funext α p l
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = takeWhileTR.go p l l #[]
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = takeWhileTR p l
simp [takeWhileTR]
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = takeWhileTR.go p l l #[]
suffices ∀ xs acc, l = acc.data ++ xs →
    takeWhileTR.go p l xs acc = acc.data ++ xs.takeWhile p from
  (this l #[] (by simp)).symm
case h.h.h
α : Type u_1
p : α → Bool
l xs : List α
⊢ ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
intro xs
no goals
α : Type u_1
p : α → Bool
l : List α
this : ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
⊢ l = #[].data ++ l
simp
no goals
case h.h.h.nil
α : Type u_1
p : α → Bool
l : List α
acc : Array α
⊢ l = acc.data ++ [] → takeWhileTR.go p l [] acc = acc.data ++ takeWhile p []
simp [takeWhile, takeWhileTR.go]
case h.h.h.cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
⊢ l = acc.data ++ x :: xs →
    (bif p x then takeWhileTR.go p l xs (Array.push acc x) else acc.data) =
      acc.data ++
        match p x with
        | true => x :: takeWhile p xs
        | false => []
case h.h.h.cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
⊢ l = acc.data ++ x :: xs → takeWhileTR.go p l (x :: xs) acc = acc.data ++ takeWhile p (x :: xs)
simp [takeWhile, takeWhileTR.go]
case h.h.h.cons.h_1
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
⊢ l = acc.data ++ x :: xs → takeWhileTR.go p l xs (Array.push acc x) = acc.data ++ x :: takeWhile p xs
case h.h.h.cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
⊢ l = acc.data ++ x :: xs →
    (bif p x then takeWhileTR.go p l xs (Array.push acc x) else acc.data) =
      acc.data ++
        match p x with
        | true => x :: takeWhile p xs
        | false => []
split <;> simp [*]
case h.h.h.cons.h_1
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.data ++ x :: xs
⊢ takeWhileTR.go p l xs (Array.push acc x) = acc.data ++ x :: takeWhile p xs
case h.h.h.cons.h_1
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
⊢ l = acc.data ++ x :: xs → takeWhileTR.go p l xs (Array.push acc x) = acc.data ++ x :: takeWhile p xs
intro h
case h.h.h.cons.h_1
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.data ++ x :: xs
⊢ (Array.push acc x).data ++ takeWhile p xs = acc.data ++ x :: takeWhile p xs

case h.h.h.cons.h_1.a
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
case h.h.h.cons.h_1
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.data ++ x :: xs
⊢ takeWhileTR.go p l xs (Array.push acc x) = acc.data ++ x :: takeWhile p xs
rw [IH]
case h.h.h.cons.h_1.a
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
case h.h.h.cons.h_1
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.data ++ x :: xs
⊢ (Array.push acc x).data ++ takeWhile p xs = acc.data ++ x :: takeWhile p xs

case h.h.h.cons.h_1.a
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
simp
case h.h.h.cons.h_1.a
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.data ++ x :: xs
⊢ l = acc.data ++ x :: xs
case h.h.h.cons.h_1.a
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
simp
no goals
case h.h.h.cons.h_1.a
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → takeWhileTR.go p l xs acc = acc.data ++ takeWhile p xs
acc : Array α
x✝ : Bool
heq✝ : p x = true
h : l = acc.data ++ x :: xs
⊢ l = acc.data ++ x :: xs
exact h