-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_eq_nil_iff {l} : filterMap f l = [] ↔ ∀ a ∈ l, f a = none

Proof state:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : List α✝¹
⊢ filterMap f l = [] → ∀ (a : α✝¹), a ∈ l → f a = none

Tactic:
exact forall_none_of_filterMap_eq_nil

Result:
no goals

Proof state:
case mpr.cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (∀ (a : α✝¹), a ∈ l → f a = none) → filterMap f l = []
h : ∀ (a_1 : α✝¹), a_1 ∈ a :: l → f a_1 = none
⊢ (match f a with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    []

Tactic:
split

Result:
case mpr.cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (∀ (a : α✝¹), a ∈ l → f a = none) → filterMap f l = []
h : ∀ (a_1 : α✝¹), a_1 ∈ a :: l → f a_1 = none
x✝ : Option α✝
heq✝ : f a = none
⊢ filterMap f l = []

case mpr.cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (∀ (a : α✝¹), a ∈ l → f a = none) → filterMap f l = []
h : ∀ (a_1 : α✝¹), a_1 ∈ a :: l → f a_1 = none
x✝ : Option α✝
b✝ : α✝
heq✝ : f a = some b✝
⊢ b✝ :: filterMap f l = []

Proof state:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : List α✝¹
⊢ (∀ (a : α✝¹), a ∈ l → f a = none) → filterMap f l = []

Tactic:
intro h

Result:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : List α✝¹
h : ∀ (a : α✝¹), a ∈ l → f a = none
⊢ filterMap f l = []

Proof state:
case mpr.cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (∀ (a : α✝¹), a ∈ l → f a = none) → filterMap f l = []
h : ∀ (a_1 : α✝¹), a_1 ∈ a :: l → f a_1 = none
x✝ : Option α✝
heq✝ : f a = none
⊢ ∀ (a : α✝¹), a ∈ l → f a = none

Tactic:
simp_all

Result:
no goals

Proof state:
case mpr.cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (∀ (a : α✝¹), a ∈ l → f a = none) → filterMap f l = []
h : ∀ (a_1 : α✝¹), a_1 ∈ a :: l → f a_1 = none
x✝ : Option α✝
heq✝ : f a = none
⊢ filterMap f l = []

Tactic:
apply ih

Result:
case mpr.cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (∀ (a : α✝¹), a ∈ l → f a = none) → filterMap f l = []
h : ∀ (a_1 : α✝¹), a_1 ∈ a :: l → f a_1 = none
x✝ : Option α✝
heq✝ : f a = none
⊢ ∀ (a : α✝¹), a ∈ l → f a = none

Proof state:
case mpr.cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (∀ (a : α✝¹), a ∈ l → f a = none) → filterMap f l = []
h : ∀ (a_1 : α✝¹), a_1 ∈ a :: l → f a_1 = none
x✝ : Option α✝
b✝ : α✝
heq✝ : f a = some b✝
⊢ b✝ :: filterMap f l = []

Tactic:
simp_all

Result:
no goals

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : List α✝¹
⊢ filterMap f l = [] ↔ ∀ (a : α✝¹), a ∈ l → f a = none

Tactic:
constructor

Result:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : List α✝¹
⊢ filterMap f l = [] → ∀ (a : α✝¹), a ∈ l → f a = none

case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : List α✝¹
⊢ (∀ (a : α✝¹), a ∈ l → f a = none) → filterMap f l = []

Proof state:
case mpr.nil
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
h : ∀ (a : α✝¹), a ∈ [] → f a = none
⊢ filterMap f [] = []

Tactic:
rfl

Result:
no goals

Proof state:
case mpr.cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (∀ (a : α✝¹), a ∈ l → f a = none) → filterMap f l = []
h : ∀ (a_1 : α✝¹), a_1 ∈ a :: l → f a_1 = none
⊢ filterMap f (a :: l) = []

Tactic:
simp only [filterMap_cons]

Result:
case mpr.cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (∀ (a : α✝¹), a ∈ l → f a = none) → filterMap f l = []
h : ∀ (a_1 : α✝¹), a_1 ∈ a :: l → f a_1 = none
⊢ (match f a with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    []