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

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

case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys

State before:
case mp
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ∨ x ∈ ys → x ∈ xs ++ ys

case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
Tactic:
. intros hf
  cases hf with
  | inl hxs => apply mem_append_front _ _ _ hxs
  | inr hys => apply mem_append_back _ _ _ hys
State after:
case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys

State before:
case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
Tactic:
. intros hb
  induction xs with
  | nil => exact Or.intro_right _ hb
  | cons z xs ih =>
    cases hb with
    | head _ => apply Or.intro_left _ (List.Mem.head _)
    | tail _ h' =>
      cases ys with
      | nil =>
        apply Or.intro_left
        apply List.Mem.tail
        simp at h'
        exact h'
      | cons y ys =>
        simp at h'
        cases ih h' with
        | inl hxxs =>
          apply Or.intro_left
          exact List.Mem.tail _ hxxs
        | inr hxys =>
          exact Or.intro_right _ hxys
State after:
no goals

State before:
case mp
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ∨ x ∈ ys → x ∈ xs ++ ys
Tactic:
intros hf
State after:
case mp
α : Type u_1
x : α
xs ys : List α
hf : x ∈ xs ∨ x ∈ ys
⊢ x ∈ xs ++ ys

State before:
case mp
α : Type u_1
x : α
xs ys : List α
hf : x ∈ xs ∨ x ∈ ys
⊢ x ∈ xs ++ ys
Tactic:
cases hf with
| inl hxs => apply mem_append_front _ _ _ hxs
| inr hys => apply mem_append_back _ _ _ hys
State after:
no goals

State before:
case mp.inl
α : Type u_1
x : α
xs ys : List α
hxs : x ∈ xs
⊢ x ∈ xs ++ ys
Tactic:
apply mem_append_front _ _ _ hxs
State after:
no goals

State before:
case mp.inr
α : Type u_1
x : α
xs ys : List α
hys : x ∈ ys
⊢ x ∈ xs ++ ys
Tactic:
apply mem_append_back _ _ _ hys
State after:
no goals

State before:
case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
Tactic:
intros hb
State after:
case mpr
α : Type u_1
x : α
xs ys : List α
hb : x ∈ xs ++ ys
⊢ x ∈ xs ∨ x ∈ ys

State before:
case mpr
α : Type u_1
x : α
xs ys : List α
hb : x ∈ xs ++ ys
⊢ x ∈ xs ∨ x ∈ ys
Tactic:
induction xs with
| nil => exact Or.intro_right _ hb
| cons z xs ih =>
  cases hb with
  | head _ => apply Or.intro_left _ (List.Mem.head _)
  | tail _ h' =>
    cases ys with
    | nil =>
      apply Or.intro_left
      apply List.Mem.tail
      simp at h'
      exact h'
    | cons y ys =>
      simp at h'
      cases ih h' with
      | inl hxxs =>
        apply Or.intro_left
        exact List.Mem.tail _ hxxs
      | inr hxys =>
        exact Or.intro_right _ hxys
State after:
no goals

State before:
case mpr.nil
α : Type u_1
x : α
ys : List α
hb : x ∈ [] ++ ys
⊢ x ∈ [] ∨ x ∈ ys
Tactic:
exact Or.intro_right _ hb
State after:
no goals

State before:
case mpr.cons
α : Type u_1
x : α
ys : List α
z : α
xs : List α
ih : x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
hb : x ∈ z :: xs ++ ys
⊢ x ∈ z :: xs ∨ x ∈ ys
Tactic:
cases hb with
| head _ => apply Or.intro_left _ (List.Mem.head _)
| tail _ h' =>
  cases ys with
  | nil =>
    apply Or.intro_left
    apply List.Mem.tail
    simp at h'
    exact h'
  | cons y ys =>
    simp at h'
    cases ih h' with
    | inl hxxs =>
      apply Or.intro_left
      exact List.Mem.tail _ hxxs
    | inr hxys =>
      exact Or.intro_right _ hxys
State after:
no goals

State before:
case mpr.cons.head
α : Type u_1
x : α
ys xs : List α
ih : x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
⊢ x ∈ x :: xs ∨ x ∈ ys
Tactic:
apply Or.intro_left _ (List.Mem.head _)
State after:
no goals

State before:
case mpr.cons.tail
α : Type u_1
x : α
ys : List α
z : α
xs : List α
ih : x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
h' : Mem x (List.append xs ys)
⊢ x ∈ z :: xs ∨ x ∈ ys
Tactic:
cases ys with
| nil =>
  apply Or.intro_left
  apply List.Mem.tail
  simp at h'
  exact h'
| cons y ys =>
  simp at h'
  cases ih h' with
  | inl hxxs =>
    apply Or.intro_left
    exact List.Mem.tail _ hxxs
  | inr hxys =>
    exact Or.intro_right _ hxys
State after:
no goals

State before:
case mpr.cons.tail.nil
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ x ∈ z :: xs ∨ x ∈ []
Tactic:
apply Or.intro_left
State after:
case mpr.cons.tail.nil.h
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ x ∈ z :: xs

State before:
case mpr.cons.tail.nil.h
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ x ∈ z :: xs
Tactic:
apply List.Mem.tail
State after:
case mpr.cons.tail.nil.h.a
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ Mem x xs

State before:
case mpr.cons.tail.nil.h.a
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ Mem x xs
Tactic:
simp at h'
State after:
case mpr.cons.tail.nil.h.a
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x xs
⊢ Mem x xs

State before:
case mpr.cons.tail.nil.h.a
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x xs
⊢ Mem x xs
Tactic:
exact h'
State after:
no goals

State before:
case mpr.cons.tail.cons
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (List.append xs (y :: ys))
⊢ x ∈ z :: xs ∨ x ∈ y :: ys
Tactic:
simp at h'
State after:
case mpr.cons.tail.cons
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
⊢ x ∈ z :: xs ∨ x ∈ y :: ys

State before:
case mpr.cons.tail.cons
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
⊢ x ∈ z :: xs ∨ x ∈ y :: ys
Tactic:
cases ih h' with
| inl hxxs =>
  apply Or.intro_left
  exact List.Mem.tail _ hxxs
| inr hxys =>
  exact Or.intro_right _ hxys
State after:
no goals

State before:
case mpr.cons.tail.cons.inl
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
hxxs : x ∈ xs
⊢ x ∈ z :: xs ∨ x ∈ y :: ys
Tactic:
apply Or.intro_left
State after:
case mpr.cons.tail.cons.inl.h
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
hxxs : x ∈ xs
⊢ x ∈ z :: xs

State before:
case mpr.cons.tail.cons.inl.h
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
hxxs : x ∈ xs
⊢ x ∈ z :: xs
Tactic:
exact List.Mem.tail _ hxxs
State after:
no goals

State before:
case mpr.cons.tail.cons.inr
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
hxys : x ∈ y :: ys
⊢ x ∈ z :: xs ∨ x ∈ y :: ys
Tactic:
exact Or.intro_right _ hxys
State after:
no goals