case nil
ι : Type ?u.417345
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ : α → Bool
l : List α
p q : α → Bool
⊢ takeWhile p (takeWhile q []) = takeWhile (fun a => decide (p a = true ∧ q a = true)) []

case cons
ι : Type ?u.417345
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ : α → Bool
l : List α
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a => decide (p a = true ∧ q a = true)) tl
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a => decide (p a = true ∧ q a = true)) (hd :: tl)
ι : Type ?u.417345
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ : α → Bool
l✝ : List α
p q : α → Bool
l : List α
⊢ takeWhile p (takeWhile q l) = takeWhile (fun a => decide (p a = true ∧ q a = true)) l
induction' l with hd tl IH
no goals
case nil
ι : Type ?u.417345
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ : α → Bool
l : List α
p q : α → Bool
⊢ takeWhile p (takeWhile q []) = takeWhile (fun a => decide (p a = true ∧ q a = true)) []
simp [takeWhile]
no goals
case cons
ι : Type ?u.417345
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p✝ : α → Bool
l : List α
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a => decide (p a = true ∧ q a = true)) tl
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a => decide (p a = true ∧ q a = true)) (hd :: tl)
by_cases hp : p hd <;> by_cases hq : q hd <;> simp [takeWhile, hp, hq, IH]