case nil
ι : Type ?u.412046
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (hl : 0 < length []), ¬p (nthLe [] 0 hl) = true

case cons
ι : Type ?u.412046
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < length xs), ¬p (nthLe xs 0 hl) = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < length (x :: xs)), ¬p (nthLe (x :: xs) 0 hl) = true
ι : Type ?u.412046
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
⊢ takeWhile p l = [] ↔ ∀ (hl : 0 < length l), ¬p (nthLe l 0 hl) = true
induction' l with x xs IH
case nil
ι : Type ?u.412046
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
⊢ ∀ (hl : 0 < length []), p (nthLe [] 0 hl) = false
case nil
ι : Type ?u.412046
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (hl : 0 < length []), ¬p (nthLe [] 0 hl) = true
simp [takeWhile, true_iff]
case nil
ι : Type ?u.412046
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
h : 0 < length []
⊢ p (nthLe [] 0 h) = false
case nil
ι : Type ?u.412046
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
⊢ ∀ (hl : 0 < length []), p (nthLe [] 0 hl) = false
intro h
no goals
case nil
ι : Type ?u.412046
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
h : 0 < length []
⊢ p (nthLe [] 0 h) = false
simp at h
no goals
case cons
ι : Type ?u.412046
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < length xs), ¬p (nthLe xs 0 hl) = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < length (x :: xs)), ¬p (nthLe (x :: xs) 0 hl) = true
by_cases hp : p x <;> simp [hp, takeWhile, IH, nthLe_cons]