no goals
ι : Type ?u.423975
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
⊢ takeWhile p (takeWhile p l) = takeWhile p l
simp_rw [takeWhile_takeWhile, and_self_iff, Bool.decide_coe]