case nil
α : Type u_1
p : α → Bool
n : ℕ
⊢ dropWhile p [] = [] ↔ ∀ (hl : 0 < length []), ¬p (nthLe [] 0 hl) = true

case cons
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
⊢ dropWhile p (hd :: tl) = hd :: tl ↔ ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ dropWhile p l = l ↔ ∀ (hl : 0 < length l), ¬p (nthLe l 0 hl) = true
cases' l with hd tl
case nil
α : Type u_1
p : α → Bool
n : ℕ
⊢ ∀ (hl : 0 < length []), ¬p (nthLe [] 0 hl) = true
case nil
α : Type u_1
p : α → Bool
n : ℕ
⊢ dropWhile p [] = [] ↔ ∀ (hl : 0 < length []), ¬p (nthLe [] 0 hl) = true
simp only [dropWhile, true_iff]
case nil
α : Type u_1
p : α → Bool
n : ℕ
h : 0 < length []
⊢ ¬p (nthLe [] 0 h) = true
case nil
α : Type u_1
p : α → Bool
n : ℕ
⊢ ∀ (hl : 0 < length []), ¬p (nthLe [] 0 hl) = true
intro h
case nil
α : Type u_1
p : α → Bool
n : ℕ
h : 0 < length []
a✝ : p (nthLe [] 0 h) = true
⊢ False
case nil
α : Type u_1
p : α → Bool
n : ℕ
h : 0 < length []
⊢ ¬p (nthLe [] 0 h) = true
by_contra
no goals
case nil
α : Type u_1
p : α → Bool
n : ℕ
h : 0 < length []
a✝ : p (nthLe [] 0 h) = true
⊢ False
rwa [length_nil, lt_self_iff_false] at h
case cons
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
case cons
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
⊢ dropWhile p (hd :: tl) = hd :: tl ↔ ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
rw [dropWhile]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
⊢ ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true

case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
case cons
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
refine' ⟨fun h => _, fun h => _⟩
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p (nthLe (hd :: tl) 0 hl✝) = true
⊢ False
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
⊢ ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
intro _ H
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ False
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p (nthLe (hd :: tl) 0 hl✝) = true
⊢ False
rw [nthLe, get] at H
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ hd :: tl <+ tl
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ False
refine' (cons_ne_self hd tl) (Sublist.antisymm _ (sublist_cons _ _))
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) <+
    tl
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ hd :: tl <+ tl
rw [← h]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ dropWhile p tl <+ tl
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) <+
    tl
simp only [H]
no goals
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ dropWhile p tl <+ tl
exact List.isSuffix.sublist (dropWhile_suffix p)
case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
this : ¬p (nthLe (hd :: tl) 0 (_ : 0 < Nat.succ (length tl))) = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
have := h (by simp only [length, Nat.succ_pos])
case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
this : ¬p hd = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
this : ¬p (nthLe (hd :: tl) 0 (_ : 0 < Nat.succ (length tl))) = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
rw [nthLe, get] at this
no goals
case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
this : ¬p hd = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
simp_rw [this]
no goals
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
⊢ 0 < length (hd :: tl)
simp only [length, Nat.succ_pos]