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

case cons
ι : Type ?u.385620
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
hl✝ : 0 < length (dropWhile p l)
hd : α
tl : List α
IH : ∀ (hl : 0 < length (dropWhile p tl)), ¬p (nthLe (dropWhile p tl) 0 hl) = true
hl : 0 < length (dropWhile p (hd :: tl))
⊢ ¬p (nthLe (dropWhile p (hd :: tl)) 0 hl) = true
ι : Type ?u.385620
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
hl : 0 < length (dropWhile p l)
⊢ ¬p (nthLe (dropWhile p l) 0 hl) = true
induction' l with hd tl IH
no goals
case nil
ι : Type ?u.385620
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
hl✝ : 0 < length (dropWhile p l)
hl : 0 < length (dropWhile p [])
⊢ ¬p (nthLe (dropWhile p []) 0 hl) = true
cases hl
case cons
ι : Type ?u.385620
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
hl✝ : 0 < length (dropWhile p l)
hd : α
tl : List α
IH : ∀ (hl : 0 < length (dropWhile p tl)), ¬p (nthLe (dropWhile p tl) 0 hl) = true
hl : 0 < length (dropWhile p (hd :: tl))
⊢ ¬p
        (nthLe
          (match p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          0
          (_ :
            0 <
              length
                (match p hd with
                | true => dropWhile p tl
                | false => hd :: tl))) =
      true
case cons
ι : Type ?u.385620
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
hl✝ : 0 < length (dropWhile p l)
hd : α
tl : List α
IH : ∀ (hl : 0 < length (dropWhile p tl)), ¬p (nthLe (dropWhile p tl) 0 hl) = true
hl : 0 < length (dropWhile p (hd :: tl))
⊢ ¬p (nthLe (dropWhile p (hd :: tl)) 0 hl) = true
simp only [dropWhile]
case pos
ι : Type ?u.385620
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
hl✝ : 0 < length (dropWhile p l)
hd : α
tl : List α
IH : ∀ (hl : 0 < length (dropWhile p tl)), ¬p (nthLe (dropWhile p tl) 0 hl) = true
hl : 0 < length (dropWhile p (hd :: tl))
hp : p hd = true
⊢ ¬p
        (nthLe
          (match p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          0
          (_ :
            0 <
              length
                (match p hd with
                | true => dropWhile p tl
                | false => hd :: tl))) =
      true

case neg
ι : Type ?u.385620
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
hl✝ : 0 < length (dropWhile p l)
hd : α
tl : List α
IH : ∀ (hl : 0 < length (dropWhile p tl)), ¬p (nthLe (dropWhile p tl) 0 hl) = true
hl : 0 < length (dropWhile p (hd :: tl))
hp : ¬p hd = true
⊢ ¬p
        (nthLe
          (match p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          0
          (_ :
            0 <
              length
                (match p hd with
                | true => dropWhile p tl
                | false => hd :: tl))) =
      true
case cons
ι : Type ?u.385620
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
hl✝ : 0 < length (dropWhile p l)
hd : α
tl : List α
IH : ∀ (hl : 0 < length (dropWhile p tl)), ¬p (nthLe (dropWhile p tl) 0 hl) = true
hl : 0 < length (dropWhile p (hd :: tl))
⊢ ¬p
        (nthLe
          (match p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          0
          (_ :
            0 <
              length
                (match p hd with
                | true => dropWhile p tl
                | false => hd :: tl))) =
      true
by_cases hp : p hd
no goals
case pos
ι : Type ?u.385620
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
hl✝ : 0 < length (dropWhile p l)
hd : α
tl : List α
IH : ∀ (hl : 0 < length (dropWhile p tl)), ¬p (nthLe (dropWhile p tl) 0 hl) = true
hl : 0 < length (dropWhile p (hd :: tl))
hp : p hd = true
⊢ ¬p
        (nthLe
          (match p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          0
          (_ :
            0 <
              length
                (match p hd with
                | true => dropWhile p tl
                | false => hd :: tl))) =
      true
simp [hp, IH]
no goals
case neg
ι : Type ?u.385620
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
hl✝ : 0 < length (dropWhile p l)
hd : α
tl : List α
IH : ∀ (hl : 0 < length (dropWhile p tl)), ¬p (nthLe (dropWhile p tl) 0 hl) = true
hl : 0 < length (dropWhile p (hd :: tl))
hp : ¬p hd = true
⊢ ¬p
        (nthLe
          (match p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          0
          (_ :
            0 <
              length
                (match p hd with
                | true => dropWhile p tl
                | false => hd :: tl))) =
      true
simp [hp, nthLe_cons]