-- Mathlib/Data/List/Sym.lean
theorem mk_mem_sym2 {xs : List α} {a b : α} (ha : a ∈ xs) (hb : b ∈ xs) :
    s(a, b) ∈ xs.sym2

Proof state:
case cons.inl.inr.h
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
hb : b ∈ xs
⊢ (∃ y ∈ xs, s(a, b) = s(a, y)) ∨ s(a, b) ∈ xs.sym2

Tactic:
left

Result:
case cons.inl.inr.h.h
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
hb : b ∈ xs
⊢ ∃ y ∈ xs, s(a, b) = s(a, y)

Proof state:
case cons.inl.inl.h
α : Type u_1
b : α
xs : List α
ih : b ∈ xs → b ∈ xs → s(b, b) ∈ xs.sym2
⊢ s(b, b) = s(b, b)

Tactic:
rfl

Result:
no goals

Proof state:
case cons.inr.inr.h.h
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) ∈ xs.sym2

Tactic:
exact ih ha hb

Result:
no goals

Proof state:
case cons.inl.inr
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
hb : b ∈ xs
⊢ s(a, b) = s(a, a) ∨ (∃ y ∈ xs, s(a, b) = s(a, y)) ∨ s(a, b) ∈ xs.sym2

Tactic:
right

Result:
case cons.inl.inr.h
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
hb : b ∈ xs
⊢ (∃ y ∈ xs, s(a, b) = s(a, y)) ∨ s(a, b) ∈ xs.sym2

Proof state:
case cons.inr.inr
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2

Tactic:
right

Result:
case cons.inr.inr.h
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
hb : b ∈ xs
⊢ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2

Proof state:
case cons.inr.inl.h.h
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
⊢ ∃ y ∈ xs, s(b, a) = s(b, y)

Tactic:
use a

Result:
no goals

Proof state:
case cons
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ x :: xs
hb : b ∈ x :: xs
⊢ s(a, b) ∈ (x :: xs).sym2

Tactic:
rw [mem_sym2_cons_iff]

Result:
case cons
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ x :: xs
hb : b ∈ x :: xs
⊢ s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2

Proof state:
case cons.inl.inr.h.h
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
hb : b ∈ xs
⊢ ∃ y ∈ xs, s(a, b) = s(a, y)

Tactic:
use b

Result:
no goals

Proof state:
case nil
α : Type u_1
a b : α
ha : a ∈ []
hb : b ∈ []
⊢ s(a, b) ∈ [].sym2

Tactic:
simp at ha

Result:
no goals

Proof state:
case cons
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a = x ∨ a ∈ xs
hb : b = x ∨ b ∈ xs
⊢ s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2

Tactic:
obtain (rfl | ha) := ha <;> obtain (rfl | hb) := hb

Result:
case cons.inl.inl
α : Type u_1
b : α
xs : List α
ih : b ∈ xs → b ∈ xs → s(b, b) ∈ xs.sym2
⊢ s(b, b) = s(b, b) ∨ (∃ y ∈ xs, s(b, b) = s(b, y)) ∨ s(b, b) ∈ xs.sym2

case cons.inl.inr
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
hb : b ∈ xs
⊢ s(a, b) = s(a, a) ∨ (∃ y ∈ xs, s(a, b) = s(a, y)) ∨ s(a, b) ∈ xs.sym2

case cons.inr.inl
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
⊢ s(a, b) = s(b, b) ∨ (∃ y ∈ xs, s(a, b) = s(b, y)) ∨ s(a, b) ∈ xs.sym2

case cons.inr.inr
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2

Proof state:
case cons.inl.inl
α : Type u_1
b : α
xs : List α
ih : b ∈ xs → b ∈ xs → s(b, b) ∈ xs.sym2
⊢ s(b, b) = s(b, b) ∨ (∃ y ∈ xs, s(b, b) = s(b, y)) ∨ s(b, b) ∈ xs.sym2

Tactic:
left

Result:
case cons.inl.inl.h
α : Type u_1
b : α
xs : List α
ih : b ∈ xs → b ∈ xs → s(b, b) ∈ xs.sym2
⊢ s(b, b) = s(b, b)

Proof state:
case cons.inr.inr.h
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
hb : b ∈ xs
⊢ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2

Tactic:
right

Result:
case cons.inr.inr.h.h
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) ∈ xs.sym2

Proof state:
case cons.inr.inl.h.h
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
⊢ ∃ y ∈ xs, s(a, b) = s(b, y)

Tactic:
rw [Sym2.eq_swap]

Result:
case cons.inr.inl.h.h
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
⊢ ∃ y ∈ xs, s(b, a) = s(b, y)

Proof state:
case cons.inr.inl
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
⊢ s(a, b) = s(b, b) ∨ (∃ y ∈ xs, s(a, b) = s(b, y)) ∨ s(a, b) ∈ xs.sym2

Tactic:
right

Result:
case cons.inr.inl.h
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
⊢ (∃ y ∈ xs, s(a, b) = s(b, y)) ∨ s(a, b) ∈ xs.sym2

Proof state:
case cons.inr.inl.h
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
⊢ (∃ y ∈ xs, s(a, b) = s(b, y)) ∨ s(a, b) ∈ xs.sym2

Tactic:
left

Result:
case cons.inr.inl.h.h
α : Type u_1
a b : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ xs
⊢ ∃ y ∈ xs, s(a, b) = s(b, y)

Proof state:
case cons
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ x :: xs
hb : b ∈ x :: xs
⊢ s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2

Tactic:
rw [mem_cons] at ha hb

Result:
case cons
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a = x ∨ a ∈ xs
hb : b = x ∨ b ∈ xs
⊢ s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2