case cons
α : Type u_1
β : Type u_2
f : α → Option β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : b ∈ filterMap f tail✝ ↔ ∃ a, a ∈ tail✝ ∧ f a = some b
⊢ (b ∈
      match f head✝ with
      | none => filterMap f tail✝
      | some b => b :: filterMap f tail✝) ↔
    f head✝ = some b ∨ ∃ a, a ∈ tail✝ ∧ f a = some b
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
b : β
⊢ b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b
induction l <;> simp
no goals
case cons
α : Type u_1
β : Type u_2
f : α → Option β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : b ∈ filterMap f tail✝ ↔ ∃ a, a ∈ tail✝ ∧ f a = some b
⊢ (b ∈
      match f head✝ with
      | none => filterMap f tail✝
      | some b => b :: filterMap f tail✝) ↔
    f head✝ = some b ∨ ∃ a, a ∈ tail✝ ∧ f a = some b
split <;> simp [*, eq_comm]