case cons
α✝ : Type u_1
p : α✝ → Bool
head✝ : α✝
tail✝ : List α✝
tail_ih✝ : find? p tail✝ = none ↔ ∀ (x : α✝), x ∈ tail✝ → ¬p x = true
⊢ (match p head✝ with
      | true => some head✝
      | false => find? p tail✝) =
      none ↔
    p head✝ = false ∧ ∀ (a : α✝), a ∈ tail✝ → p a = false
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
⊢ find? p l = none ↔ ∀ (x : α✝), x ∈ l → ¬p x = true
induction l <;> simp
no goals
case cons
α✝ : Type u_1
p : α✝ → Bool
head✝ : α✝
tail✝ : List α✝
tail_ih✝ : find? p tail✝ = none ↔ ∀ (x : α✝), x ∈ tail✝ → ¬p x = true
⊢ (match p head✝ with
      | true => some head✝
      | false => find? p tail✝) =
      none ↔
    p head✝ = false ∧ ∀ (a : α✝), a ∈ tail✝ → p a = false
split <;> simp [*]