Theorem: CNF.List.all_none_of_filterMap_eq_nil (LeanSAT/Reflect/CNF/Decidable.lean)

State before:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
xs : List α✝¹
h : List.filterMap f xs = []
⊢ ∀ (x : α✝¹), x ∈ xs → f x = none
Tactic:
intro x hx
State after:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
xs : List α✝¹
h : List.filterMap f xs = []
x : α✝¹
hx : x ∈ xs
⊢ f x = none

State before:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
xs : List α✝¹
h : List.filterMap f xs = []
x : α✝¹
hx : x ∈ xs
⊢ f x = none
Tactic:
induction xs with
| nil => contradiction
| cons y ys ih =>
  simp [List.filterMap] at h
  split at h
  . cases hx with
    | head => assumption
    | tail _ hmem => exact ih h hmem
  . contradiction
State after:
no goals

State before:
case nil
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x : α✝¹
h : List.filterMap f [] = []
hx : x ∈ []
⊢ f x = none
Tactic:
contradiction
State after:
no goals

State before:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
h : List.filterMap f (y :: ys) = []
hx : x ∈ y :: ys
⊢ f x = none
Tactic:
simp [List.filterMap] at h
State after:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
h :
  (match f y with
    | none => List.filterMap f ys
    | some b => b :: List.filterMap f ys) =
    []
hx : x ∈ y :: ys
⊢ f x = none

State before:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
h :
  (match f y with
    | none => List.filterMap f ys
    | some b => b :: List.filterMap f ys) =
    []
hx : x ∈ y :: ys
⊢ f x = none
Tactic:
split at h
State after:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
heq✝ : f y = none
h : List.filterMap f ys = []
⊢ f x = none

case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: List.filterMap f ys = []
⊢ f x = none

State before:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
heq✝ : f y = none
h : List.filterMap f ys = []
⊢ f x = none

case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: List.filterMap f ys = []
⊢ f x = none
Tactic:
. cases hx with
  | head => assumption
  | tail _ hmem => exact ih h hmem
State after:
case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: List.filterMap f ys = []
⊢ f x = none

State before:
case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: List.filterMap f ys = []
⊢ f x = none
Tactic:
. contradiction
State after:
no goals

State before:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
heq✝ : f y = none
h : List.filterMap f ys = []
⊢ f x = none
Tactic:
cases hx with
| head => assumption
| tail _ hmem => exact ih h hmem
State after:
no goals

State before:
case cons.h_1.head
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
x✝ : Option α✝
h : List.filterMap f ys = []
heq✝ : f x = none
⊢ f x = none
Tactic:
assumption
State after:
no goals

State before:
case cons.h_1.tail
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
x✝ : Option α✝
heq✝ : f y = none
h : List.filterMap f ys = []
hmem : List.Mem x ys
⊢ f x = none
Tactic:
exact ih h hmem
State after:
no goals

State before:
case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: List.filterMap f ys = []
⊢ f x = none
Tactic:
contradiction
State after:
no goals