Theorem: List.mem_cons_iff_mem_singleton_or_tail (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ y :: ys ↔ x ∈ [y] ∨ x ∈ ys
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ y :: ys → x ∈ [y] ∨ x ∈ ys

case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys

State before:
case mp
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ y :: ys → x ∈ [y] ∨ x ∈ ys

case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys
Tactic:
. intro hf
  cases hf with
  | head => apply Or.intro_left _ (Mem.head _)
  | tail _ h => apply Or.intro_right _ h
State after:
case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys

State before:
case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys
Tactic:
. intro hb
  cases hb with
  | inl h => rw [(mem_singleton_iff x y).mp h]; apply Mem.head
  | inr h => apply Mem.tail _ h
State after:
no goals

State before:
case mp
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ y :: ys → x ∈ [y] ∨ x ∈ ys
Tactic:
intro hf
State after:
case mp
α : Type u_1
y : α
ys : List α
x : α
hf : x ∈ y :: ys
⊢ x ∈ [y] ∨ x ∈ ys

State before:
case mp
α : Type u_1
y : α
ys : List α
x : α
hf : x ∈ y :: ys
⊢ x ∈ [y] ∨ x ∈ ys
Tactic:
cases hf with
| head => apply Or.intro_left _ (Mem.head _)
| tail _ h => apply Or.intro_right _ h
State after:
no goals

State before:
case mp.head
α : Type u_1
y : α
ys : List α
⊢ y ∈ [y] ∨ y ∈ ys
Tactic:
apply Or.intro_left _ (Mem.head _)
State after:
no goals

State before:
case mp.tail
α : Type u_1
y : α
ys : List α
x : α
h : Mem x ys
⊢ x ∈ [y] ∨ x ∈ ys
Tactic:
apply Or.intro_right _ h
State after:
no goals

State before:
case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys
Tactic:
intro hb
State after:
case mpr
α : Type u_1
y : α
ys : List α
x : α
hb : x ∈ [y] ∨ x ∈ ys
⊢ x ∈ y :: ys

State before:
case mpr
α : Type u_1
y : α
ys : List α
x : α
hb : x ∈ [y] ∨ x ∈ ys
⊢ x ∈ y :: ys
Tactic:
cases hb with
| inl h => rw [(mem_singleton_iff x y).mp h]; apply Mem.head
| inr h => apply Mem.tail _ h
State after:
no goals

State before:
case mpr.inl
α : Type u_1
y : α
ys : List α
x : α
h : x ∈ [y]
⊢ x ∈ y :: ys
Tactic:
rw [(mem_singleton_iff x y).mp h]
State after:
case mpr.inl
α : Type u_1
y : α
ys : List α
x : α
h : x ∈ [y]
⊢ y ∈ y :: ys

State before:
case mpr.inl
α : Type u_1
y : α
ys : List α
x : α
h : x ∈ [y]
⊢ y ∈ y :: ys
Tactic:
apply Mem.head
State after:
no goals

State before:
case mpr.inr
α : Type u_1
y : α
ys : List α
x : α
h : x ∈ ys
⊢ x ∈ y :: ys
Tactic:
apply Mem.tail _ h
State after:
no goals