-- Mathlib/Data/List/Sym.lean
theorem mem_of_mem_of_mem_sym {n : ℕ} {xs : List α} {a : α} {z : Sym α n}
    (ha : a ∈ z) (hz : z ∈ xs.sym n) : a ∈ xs :=
  match n, xs with
  | 0, xs => by
    cases Sym.eq_nil_of_card_zero z
    simp at ha
  | n + 1, [] => by simp [List.sym] at hz
  | n + 1, x :: xs => by
    rw [List.sym, mem_append, mem_map] at hz
    obtain ⟨z, hz, rfl⟩ | hz := hz
    · rw [Sym.mem_cons] at ha
      obtain rfl | ha := ha
      · simp
      · exact mem_of_mem_of_mem_sym ha hz
    · rw [mem_cons]
      right
      exact mem_of_mem_of_mem_sym ha hz

Proof state:
case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a ∈ x :: xs

Tactic:
rw [mem_cons]

Result:
case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a = x ∨ a ∈ xs

Proof state:
case refl
α : Type u_1
n : ℕ
xs✝ : List α
a : α
xs : List α
ha : a ∈ Sym.nil
hz : Sym.nil ∈ List.sym 0 xs
⊢ a ∈ xs

Tactic:
simp at ha

Result:
no goals

Proof state:
case inr.h
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a ∈ xs

Tactic:
exact mem_of_mem_of_mem_sym ha hz

Result:
no goals

Proof state:
case inl.intro.intro
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a = x ∨ a ∈ z
⊢ a ∈ x :: xs

Tactic:
obtain rfl | ha := ha

Result:
case inl.intro.intro.inl
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
xs : List α
z : Sym α n
hz : z ∈ List.sym n (a :: xs)
⊢ a ∈ a :: xs

case inl.intro.intro.inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a ∈ z
⊢ a ∈ x :: xs

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) (x :: xs)
⊢ a ∈ x :: xs

Tactic:
rw [List.sym, mem_append, mem_map] at hz

Result:
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ z ∈ List.sym (n + 1) xs
⊢ a ∈ x :: xs

Proof state:
case inl.intro.intro
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a ∈ x ::ₛ z
⊢ a ∈ x :: xs

Tactic:
rw [Sym.mem_cons] at ha

Result:
case inl.intro.intro
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a = x ∨ a ∈ z
⊢ a ∈ x :: xs

Proof state:
case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a = x ∨ a ∈ xs

Tactic:
right

Result:
case inr.h
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a ∈ xs

Proof state:
case inl.intro.intro.inl
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
xs : List α
z : Sym α n
hz : z ∈ List.sym n (a :: xs)
⊢ a ∈ a :: xs

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n✝ : ℕ
xs : List α
a : α
n : ℕ
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) []
⊢ a ∈ []

Tactic:
simp [List.sym] at hz

Result:
no goals

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ z ∈ List.sym (n + 1) xs
⊢ a ∈ x :: xs

Tactic:
obtain ⟨z, hz, rfl⟩ | hz := hz

Result:
case inl.intro.intro
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a ∈ x ::ₛ z
⊢ a ∈ x :: xs

case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a ∈ x :: xs

Proof state:
α : Type u_1
n : ℕ
xs✝ : List α
a : α
xs : List α
z : Sym α 0
ha : a ∈ z
hz : z ∈ List.sym 0 xs
⊢ a ∈ xs

Tactic:
cases Sym.eq_nil_of_card_zero z

Result:
case refl
α : Type u_1
n : ℕ
xs✝ : List α
a : α
xs : List α
ha : a ∈ Sym.nil
hz : Sym.nil ∈ List.sym 0 xs
⊢ a ∈ xs

Proof state:
case inl.intro.intro.inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a ∈ z
⊢ a ∈ x :: xs

Tactic:
exact mem_of_mem_of_mem_sym ha hz

Result:
no goals