-- Mathlib/Data/List/TakeWhile.lean
theorem dropWhile_get_zero_not (l : List α) (hl : 0 < (l.dropWhile p).length) :
    ¬p ((l.dropWhile p).get ⟨0, hl⟩)

Proof state:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
hl : 0 < (dropWhile p (hd :: tl)).length
hp✝ : p hd = true
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p (dropWhile p tl)[0] = true
hp : p hd = true
⊢ 0 < (dropWhile p tl).length

Tactic:
simp_all only [dropWhile_cons_of_pos]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
hl : 0 < (dropWhile p []).length
⊢ ¬p ((dropWhile p []).get ⟨0, hl⟩) = true

Tactic:
cases hl

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
hl : 0 < (dropWhile p l).length
⊢ ¬p ((dropWhile p l).get ⟨0, hl⟩) = true

Tactic:
induction' l with hd tl IH

Result:
case nil
α : Type u_1
p : α → Bool
hl : 0 < (dropWhile p []).length
⊢ ¬p ((dropWhile p []).get ⟨0, hl⟩) = true

case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
⊢ ¬p ((dropWhile p (hd :: tl)).get ⟨0, hl⟩) = true

Proof state:
case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

Tactic:
by_cases hp : p hd

Result:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

case neg
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : ¬p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

Proof state:
case neg
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : ¬p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

Tactic:
simp [hp]

Result:
no goals

Proof state:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
hl : 0 < (dropWhile p (hd :: tl)).length
hp✝ : p hd = true
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p (dropWhile p tl)[0] = true
hp : p hd = true
⊢ ¬p (dropWhile p tl)[0] = true

Tactic:
apply IH

Result:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
hl : 0 < (dropWhile p (hd :: tl)).length
hp✝ : p hd = true
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p (dropWhile p tl)[0] = true
hp : p hd = true
⊢ 0 < (dropWhile p tl).length

Proof state:
case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
⊢ ¬p ((dropWhile p (hd :: tl)).get ⟨0, hl⟩) = true

Tactic:
simp only [dropWhile]

Result:
case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

Proof state:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

Tactic:
simp_all only [get_eq_getElem]

Result:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
hl : 0 < (dropWhile p (hd :: tl)).length
hp✝ : p hd = true
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p (dropWhile p tl)[0] = true
hp : p hd = true
⊢ ¬p (dropWhile p tl)[0] = true