-- Mathlib/Data/List/Sym.lean
theorem dedup_sym2 [DecidableEq α] (xs : List α) : xs.sym2.dedup = xs.dedup.sym2

Proof state:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ (map (fun y => s(x, y)) xs).Disjoint xs.sym2

Tactic:
exact map_mk_disjoint_sym2 x xs hm

Result:
no goals

Proof state:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ s(x, x) ∈ map (fun y => s(x, y)) xs ++ xs.sym2

Tactic:
refine mem_append_left _ ?_

Result:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ s(x, x) ∈ map (fun y => s(x, y)) xs

Proof state:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ (s(x, x) :: (map (fun y => s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

Tactic:
rw [dedup_cons_of_mem hm, ← ih, dedup_cons_of_mem,
  List.Subset.dedup_append_right (map_mk_sublist_sym2 _ _ hm).subset]

Result:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ s(x, x) ∈ map (fun y => s(x, y)) xs ++ xs.sym2

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].sym2.dedup = [].dedup.sym2

Tactic:
simp only [List.sym2, dedup_nil]

Result:
no goals

Proof state:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ s(x, x) ∈ map (fun y => s(x, y)) xs

Tactic:
rw [mem_map]

Result:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ ∃ a ∈ xs, s(x, a) = s(x, x)

Proof state:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) ∉ map (fun y => s(x, y)) xs ++ xs.sym2

Tactic:
simp [hm, mem_sym2_iff]

Result:
no goals

Proof state:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ (s(x, x) :: (map (fun y => s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

Tactic:
rw [dedup_cons_of_not_mem hm, List.sym2, map_cons, ← ih, dedup_cons_of_not_mem, cons_append,
  List.Disjoint.dedup_append, dedup_map_of_injective]

Result:
case cons.inr.hf
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ Function.Injective fun y => s(x, y)

case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ (map (fun y => s(x, y)) xs).Disjoint xs.sym2

case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) ∉ map (fun y => s(x, y)) xs ++ xs.sym2

Proof state:
case cons.inr.hf
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ Function.Injective fun y => s(x, y)

Tactic:
exact (Sym2.mkEmbedding _).injective

Result:
no goals

Proof state:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ ∃ a ∈ xs, s(x, a) = s(x, x)

Tactic:
exact ⟨_, hm, Sym2.eq_swap⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
⊢ (x :: xs).sym2.dedup = (x :: xs).dedup.sym2

Tactic:
simp only [List.sym2, map_cons, cons_append]

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
⊢ (s(x, x) :: (map (fun y => s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
⊢ (s(x, x) :: (map (fun y => s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

Tactic:
obtain hm | hm := Decidable.em (x ∈ xs)

Result:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ (s(x, x) :: (map (fun y => s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ (s(x, x) :: (map (fun y => s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2