-- Mathlib/Data/List/DropRight.lean
theorem dropWhile_eq_self_iff : dropWhile p l = l ↔ ∀ hl : 0 < l.length, ¬p (l.get ⟨0, hl⟩)

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

Tactic:
rw [get] at this

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

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

Tactic:
intro h

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

Proof state:
case nil
α : Type u_1
p : α → Bool
h : 0 < [].length
a✝ : p ([].get ⟨0, h⟩) = true
⊢ False

Tactic:
rwa [length_nil, lt_self_iff_false] at h

Result:
no goals

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

Tactic:
by_contra

Result:
case nil
α : Type u_1
p : α → Bool
h : 0 < [].length
a✝ : p ([].get ⟨0, h⟩) = true
⊢ False

Proof state:
case cons.refine_1
α : Type u_1
p : α → Bool
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < (hd :: tl).length
H : p hd = true
⊢ False

Tactic:
refine (cons_ne_self hd tl) (Sublist.antisymm ?_ (sublist_cons_self _ _))

Result:
case cons.refine_1
α : Type u_1
p : α → Bool
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < (hd :: tl).length
H : p hd = true
⊢ hd :: tl <+ tl

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

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

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

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

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

Tactic:
simp_rw [this]

Result:
no goals

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

Tactic:
intro _ H

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

Proof state:
case cons.refine_1
α : Type u_1
p : α → Bool
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < (hd :: tl).length
H : p hd = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) <+
    tl

Tactic:
simp only [H]

Result:
case cons.refine_1
α : Type u_1
p : α → Bool
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < (hd :: tl).length
H : p hd = true
⊢ dropWhile p tl <+ tl

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

Tactic:
simp only [dropWhile, true_iff]

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

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

Tactic:
simp only [length, Nat.succ_pos]

Result:
no goals

Proof state:
case cons.refine_1
α : Type u_1
p : α → Bool
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < (hd :: tl).length
H : p hd = true
⊢ hd :: tl <+ tl

Tactic:
rw [← h]

Result:
case cons.refine_1
α : Type u_1
p : α → Bool
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < (hd :: tl).length
H : p hd = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) <+
    tl

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

Tactic:
have := h (by simp only [length, Nat.succ_pos])

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

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

Tactic:
rw [get] at H

Result:
case cons.refine_1
α : Type u_1
p : α → Bool
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < (hd :: tl).length
H : p hd = true
⊢ False

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

Tactic:
rw [dropWhile]

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

Proof state:
case cons.refine_1
α : Type u_1
p : α → Bool
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < (hd :: tl).length
H : p hd = true
⊢ dropWhile p tl <+ tl

Tactic:
exact List.IsSuffix.sublist (dropWhile_suffix p)

Result:
no goals

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

Tactic:
rcases l with - | ⟨hd, tl⟩

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

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