case nil
ι : Type ?u.387507
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
⊢ dropWhile p [] = [] ↔ ∀ (x : α), x ∈ [] → p x = true

case cons
ι : Type ?u.387507
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
ι : Type ?u.387507
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
⊢ dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true
induction' l with x xs IH
no goals
case nil
ι : Type ?u.387507
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
⊢ dropWhile p [] = [] ↔ ∀ (x : α), x ∈ [] → p x = true
simp [dropWhile]
no goals
case cons
ι : Type ?u.387507
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
by_cases hp : p x <;> simp [hp, dropWhile, IH]