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

State before:
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs ↔ x ∈ reverse xs
Tactic:
rw [reverse_eq_reverseSpec]
State after:
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs ↔ x ∈ reverseSpec xs

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

case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs

State before:
case mp
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs → x ∈ reverseSpec xs

case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs
Tactic:
. intro hf
  induction hf with
  | head xs =>
    simp only [reverseSpec]
    apply mem_append_singleton
  | @tail y ys h_x_ys ih =>
    simp only [reverseSpec]
    apply mem_append_front _ _ _ ih
State after:
case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs

State before:
case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs
Tactic:
. intro hb
  induction xs with
  | nil => contradiction
  | cons y ys ih =>
    simp only [reverseSpec] at hb
    rw [List.mem_append_comm] at hb
    simp only [HAppend.hAppend, Append.append, List.append] at hb
    cases hb with
    | head => exact Mem.head _
    | tail _ htail => exact Mem.tail _ (ih htail)
State after:
no goals

State before:
case mp
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs → x ∈ reverseSpec xs
Tactic:
intro hf
State after:
case mp
α : Type u_1
x : α
xs : List α
hf : x ∈ xs
⊢ x ∈ reverseSpec xs

State before:
case mp
α : Type u_1
x : α
xs : List α
hf : x ∈ xs
⊢ x ∈ reverseSpec xs
Tactic:
induction hf with
| head xs =>
  simp only [reverseSpec]
  apply mem_append_singleton
| @tail y ys h_x_ys ih =>
  simp only [reverseSpec]
  apply mem_append_front _ _ _ ih
State after:
no goals

State before:
case mp.head
α : Type u_1
x : α
xs✝ xs : List α
⊢ x ∈ reverseSpec (x :: xs)
Tactic:
simp only [reverseSpec]
State after:
case mp.head
α : Type u_1
x : α
xs✝ xs : List α
⊢ x ∈ reverseSpec xs ++ [x]

State before:
case mp.head
α : Type u_1
x : α
xs✝ xs : List α
⊢ x ∈ reverseSpec xs ++ [x]
Tactic:
apply mem_append_singleton
State after:
no goals

State before:
case mp.tail
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h_x_ys : Mem x ys
ih : x ∈ reverseSpec ys
⊢ x ∈ reverseSpec (y :: ys)
Tactic:
simp only [reverseSpec]
State after:
case mp.tail
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h_x_ys : Mem x ys
ih : x ∈ reverseSpec ys
⊢ x ∈ reverseSpec ys ++ [y]

State before:
case mp.tail
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h_x_ys : Mem x ys
ih : x ∈ reverseSpec ys
⊢ x ∈ reverseSpec ys ++ [y]
Tactic:
apply mem_append_front _ _ _ ih
State after:
no goals

State before:
case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs
Tactic:
intro hb
State after:
case mpr
α : Type u_1
x : α
xs : List α
hb : x ∈ reverseSpec xs
⊢ x ∈ xs

State before:
case mpr
α : Type u_1
x : α
xs : List α
hb : x ∈ reverseSpec xs
⊢ x ∈ xs
Tactic:
induction xs with
| nil => contradiction
| cons y ys ih =>
  simp only [reverseSpec] at hb
  rw [List.mem_append_comm] at hb
  simp only [HAppend.hAppend, Append.append, List.append] at hb
  cases hb with
  | head => exact Mem.head _
  | tail _ htail => exact Mem.tail _ (ih htail)
State after:
no goals

State before:
case mpr.nil
α : Type u_1
x : α
hb : x ∈ reverseSpec []
⊢ x ∈ []
Tactic:
contradiction
State after:
no goals

State before:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ reverseSpec (y :: ys)
⊢ x ∈ y :: ys
Tactic:
simp only [reverseSpec] at hb
State after:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ reverseSpec ys ++ [y]
⊢ x ∈ y :: ys

State before:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ reverseSpec ys ++ [y]
⊢ x ∈ y :: ys
Tactic:
rw [List.mem_append_comm] at hb
State after:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ [y] ++ reverseSpec ys
⊢ x ∈ y :: ys

State before:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ [y] ++ reverseSpec ys
⊢ x ∈ y :: ys
Tactic:
simp only [HAppend.hAppend, Append.append, List.append] at hb
State after:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ y :: reverseSpec ys
⊢ x ∈ y :: ys

State before:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ y :: reverseSpec ys
⊢ x ∈ y :: ys
Tactic:
cases hb with
| head => exact Mem.head _
| tail _ htail => exact Mem.tail _ (ih htail)
State after:
no goals

State before:
case mpr.cons.head
α : Type u_1
x : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
⊢ x ∈ x :: ys
Tactic:
exact Mem.head _
State after:
no goals

State before:
case mpr.cons.tail
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
htail : Mem x (reverseSpec ys)
⊢ x ∈ y :: ys
Tactic:
exact Mem.tail _ (ih htail)
State after:
no goals