-- Mathlib/Data/List/TakeWhile.lean
lemma find?_eq_head?_dropWhile_not :
    l.find? p = (l.dropWhile (fun x ↦ ! (p x))).head?

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ find? p [] = (dropWhile (fun x => !p x) []).head?

Tactic:
simp

Result:
no goals

Proof state:
case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ find? p (head :: tail) = (dropWhile (fun x => !p x) (head :: tail)).head?

Tactic:
rw [find?_cons_of_neg _ phh', dropWhile_cons_of_pos]

Result:
case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ find? p tail = (dropWhile (fun x => !p x) tail).head?

case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ (!p head) = true

Proof state:
case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : true = p head
⊢ find? p (head :: tail) = (dropWhile (fun x => !p x) (head :: tail)).head?

Tactic:
rw [find?_cons_of_pos _ phh.symm, dropWhile_cons_of_neg]

Result:
case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : true = p head
⊢ some head = (head :: tail).head?

case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : true = p head
⊢ ¬(!p head) = true

Proof state:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ find? p [] = (dropWhile (fun x => !p x) []).head?

case cons
α : Type u_1
p : α → Bool
l : List α
head✝ : α
tail✝ : List α
tail_ih✝ : find? p tail✝ = (dropWhile (fun x => !p x) tail✝).head?
⊢ find? p (head✝ :: tail✝) = (dropWhile (fun x => !p x) (head✝ :: tail✝)).head?

Tactic:
case nil => simp

Result:
case cons
α : Type u_1
p : α → Bool
l : List α
head✝ : α
tail✝ : List α
tail_ih✝ : find? p tail✝ = (dropWhile (fun x => !p x) tail✝).head?
⊢ find? p (head✝ :: tail✝) = (dropWhile (fun x => !p x) (head✝ :: tail✝)).head?

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ find? p l = (dropWhile (fun x => !p x) l).head?

Tactic:
induction l

Result:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ find? p [] = (dropWhile (fun x => !p x) []).head?

case cons
α : Type u_1
p : α → Bool
l : List α
head✝ : α
tail✝ : List α
tail_ih✝ : find? p tail✝ = (dropWhile (fun x => !p x) tail✝).head?
⊢ find? p (head✝ :: tail✝) = (dropWhile (fun x => !p x) (head✝ :: tail✝)).head?

Proof state:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
ph : Bool := p head
phh : ph = p head
⊢ find? p (head :: tail) = (dropWhile (fun x => !p x) (head :: tail)).head?

Tactic:
rcases ph with rfl | rfl

Result:
case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : false = p head
⊢ find? p (head :: tail) = (dropWhile (fun x => !p x) (head :: tail)).head?

case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : true = p head
⊢ find? p (head :: tail) = (dropWhile (fun x => !p x) (head :: tail)).head?

Proof state:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
⊢ find? p (head :: tail) = (dropWhile (fun x => !p x) (head :: tail)).head?

Tactic:
set ph := p head with phh

Result:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
ph : Bool := p head
phh : ph = p head
⊢ find? p (head :: tail) = (dropWhile (fun x => !p x) (head :: tail)).head?

Proof state:
case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ find? p tail = (dropWhile (fun x => !p x) tail).head?

Tactic:
exact hi

Result:
no goals

Proof state:
case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : false = p head
⊢ find? p (head :: tail) = (dropWhile (fun x => !p x) (head :: tail)).head?

Tactic:
have phh' : ¬(p head = true) := by simp [phh.symm]

Result:
case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ find? p (head :: tail) = (dropWhile (fun x => !p x) (head :: tail)).head?

Proof state:
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : false = p head
⊢ ¬p head = true

Tactic:
simp [phh.symm]

Result:
no goals

Proof state:
case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ (!p head) = true

Tactic:
simpa using phh

Result:
no goals

Proof state:
case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : true = p head
⊢ ¬(!p head) = true

Tactic:
simpa using phh

Result:
no goals

Proof state:
case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x => !p x) tail).head?
phh : true = p head
⊢ some head = (head :: tail).head?

Tactic:
simp

Result:
no goals