-- Mathlib/Data/List/Sym.lean
theorem map_mk_disjoint_sym2 (x : α) (xs : List α) (h : x ∉ xs) :
    (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2

Proof state:
case cons.refine_3
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ (map (fun y => s(x, y)) xs).Disjoint (map (fun y => s(x', y)) xs)

Tactic:
intro z hx hy

Result:
case cons.refine_3
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
z : Sym2 α
hx : z ∈ map (fun y => s(x, y)) xs
hy : z ∈ map (fun y => s(x', y)) xs
⊢ False

Proof state:
case cons.refine_3.intro.intro.intro.intro
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
a : α
hx✝ : a ∈ xs
b : α
hy : b ∈ xs
hx : s(x', b) = s(x, a)
⊢ False

Tactic:
simp [Sym2.mk_eq_mk_iff, Ne.symm h.1] at hx

Result:
case cons.refine_3.intro.intro.intro.intro
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
a : α
hx✝ : a ∈ xs
b : α
hy : b ∈ xs
hx : x' = a ∧ b = x
⊢ False

Proof state:
case cons.refine_1.refine_2.inr
α : Type u_1
x' : α
xs : List α
x'' : α
hx : x'' ∈ xs
ih : x'' ∉ xs → (map (fun y => s(x'', y)) xs).Disjoint xs.sym2
h : ¬x'' = x' ∧ x'' ∉ xs
⊢ False

Tactic:
exact h.2 hx

Result:
no goals

Proof state:
case cons.refine_1.refine_1
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x, x') ≠ s(x', x')

Tactic:
simp [h.1]

Result:
no goals

Proof state:
case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ (map (fun y => s(x, y)) (x' :: xs)).Disjoint (x' :: xs).sym2

Tactic:
rw [List.sym2, map_cons, map_cons, disjoint_cons_left, disjoint_append_right,
  disjoint_cons_right]

Result:
case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x, x') ∉ s(x', x') :: map (fun y => s(x', y)) xs ++ xs.sym2 ∧
    (s(x', x') ∉ map (fun y => s(x, y)) xs ∧ (map (fun y => s(x, y)) xs).Disjoint (map (fun y => s(x', y)) xs)) ∧
      (map (fun y => s(x, y)) xs).Disjoint xs.sym2

Proof state:
case cons.refine_3.intro.intro.intro.intro.intro
α : Type u_1
x' : α
xs : List α
b : α
hy : b ∈ xs
hx : x' ∈ xs
ih : b ∉ xs → (map (fun y => s(b, y)) xs).Disjoint xs.sym2
h : ¬b = x' ∧ b ∉ xs
⊢ False

Tactic:
exact h.2 hy

Result:
no goals

Proof state:
case cons.refine_4
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ (map (fun y => s(x, y)) xs).Disjoint xs.sym2

Tactic:
exact ih h.2

Result:
no goals

Proof state:
case cons.refine_3
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
z : Sym2 α
hx : ∃ a ∈ xs, s(x, a) = z
hy : ∃ a ∈ xs, s(x', a) = z
⊢ False

Tactic:
obtain ⟨a, hx, rfl⟩ := hx

Result:
case cons.refine_3.intro.intro
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
a : α
hx : a ∈ xs
hy : ∃ a_1 ∈ xs, s(x', a_1) = s(x, a)
⊢ False

Proof state:
case cons.refine_1.refine_2
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ ∀ x_1 ∈ xs, ¬s(x', x_1) = s(x, x')

Tactic:
intro x'' hx

Result:
case cons.refine_1.refine_2
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
x'' : α
hx : x'' ∈ xs
⊢ ¬s(x', x'') = s(x, x')

Proof state:
case cons.refine_1.refine_3
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x, x') ∉ xs.sym2

Tactic:
simp [mk_mem_sym2_iff, h.2]

Result:
no goals

Proof state:
case cons.refine_1
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x, x') ∉ s(x', x') :: map (fun y => s(x', y)) xs ++ xs.sym2

Tactic:
refine not_mem_cons_of_ne_of_not_mem ?_ (not_mem_append ?_ ?_)

Result:
case cons.refine_1.refine_1
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x, x') ≠ s(x', x')

case cons.refine_1.refine_2
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x, x') ∉ map (fun y => s(x', y)) xs

case cons.refine_1.refine_3
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x, x') ∉ xs.sym2

Proof state:
case cons.refine_1.refine_2
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x, x') ∉ map (fun y => s(x', y)) xs

Tactic:
simp_rw [mem_map, not_exists, not_and]

Result:
case cons.refine_1.refine_2
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ ∀ x_1 ∈ xs, ¬s(x', x_1) = s(x, x')

Proof state:
case nil
α : Type u_1
x : α
h : x ∉ []
⊢ (map (fun y => s(x, y)) []).Disjoint [].sym2

Tactic:
simp

Result:
no goals

Proof state:
case cons.refine_3
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
z : Sym2 α
hx : z ∈ map (fun y => s(x, y)) xs
hy : z ∈ map (fun y => s(x', y)) xs
⊢ False

Tactic:
rw [List.mem_map] at hx hy

Result:
case cons.refine_3
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
z : Sym2 α
hx : ∃ a ∈ xs, s(x, a) = z
hy : ∃ a ∈ xs, s(x', a) = z
⊢ False

Proof state:
case cons.refine_1.refine_2.inl.intro
α : Type u_1
xs : List α
x'' : α
hx : x'' ∈ xs
ih : x'' ∉ xs → (map (fun y => s(x'', y)) xs).Disjoint xs.sym2
h : ¬x'' = x'' ∧ x'' ∉ xs
⊢ False

Tactic:
exact h.2 hx

Result:
no goals

Proof state:
case cons.refine_1.refine_2
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
x'' : α
hx : x'' ∈ xs
⊢ ¬s(x', x'') = s(x, x')

Tactic:
simp_rw [Sym2.mk_eq_mk_iff, Prod.swap_prod_mk, Prod.mk.injEq, true_and]

Result:
case cons.refine_1.refine_2
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
x'' : α
hx : x'' ∈ xs
⊢ ¬(x' = x ∧ x'' = x' ∨ x'' = x)

Proof state:
case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : x ∉ x' :: xs
⊢ (map (fun y => s(x, y)) (x' :: xs)).Disjoint (x' :: xs).sym2

Tactic:
simp only [mem_cons, not_or] at h

Result:
case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ (map (fun y => s(x, y)) (x' :: xs)).Disjoint (x' :: xs).sym2

Proof state:
case cons.refine_1.refine_2
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
x'' : α
hx : x'' ∈ xs
⊢ ¬(x' = x ∧ x'' = x' ∨ x'' = x)

Tactic:
rintro (⟨rfl, rfl⟩ | rfl)

Result:
case cons.refine_1.refine_2.inl.intro
α : Type u_1
xs : List α
x'' : α
hx : x'' ∈ xs
ih : x'' ∉ xs → (map (fun y => s(x'', y)) xs).Disjoint xs.sym2
h : ¬x'' = x'' ∧ x'' ∉ xs
⊢ False

case cons.refine_1.refine_2.inr
α : Type u_1
x' : α
xs : List α
x'' : α
hx : x'' ∈ xs
ih : x'' ∉ xs → (map (fun y => s(x'', y)) xs).Disjoint xs.sym2
h : ¬x'' = x' ∧ x'' ∉ xs
⊢ False