-- Mathlib/Data/List/Sym.lean
theorem Perm.sym2 {xs ys : List α} (h : xs ~ ys) :
    xs.sym2 ~ ys.sym2

Proof state:
α : Type u_1
xs ys : List α
h : xs ~ ys
⊢ xs.sym2 ~ ys.sym2

Tactic:
induction h with
| nil => rfl
| cons x h ih =>
  simp only [List.sym2, map_cons, cons_append, perm_cons]
  exact (h.map _).append ih
| swap x y xs =>
  simp only [List.sym2, map_cons, cons_append]
  conv => enter [1,2,1]; rw [Sym2.eq_swap]
  refine Perm.trans (Perm.swap ..) (Perm.trans (Perm.cons _ ?_) (Perm.swap ..))
  simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe,
    ← Multiset.coe_add, ← Multiset.singleton_add]
  simp only [add_assoc, add_left_comm]
| trans _ _ ih1 ih2 => exact ih1.trans ih2

Result:
no goals

Proof state:
case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ s(y, y) :: s(y, x) :: (List.map (fun y_1 => s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y => s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: s(x, y) :: (List.map (fun y => s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 => s(y, y_1)) xs ++ xs.sym2))

Tactic:
conv => enter [1,2,1]; rw [Sym2.eq_swap]

Result:
case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ s(y, y) :: s(x, y) :: (List.map (fun y_1 => s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y => s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: s(x, y) :: (List.map (fun y => s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 => s(y, y_1)) xs ++ xs.sym2))

Proof state:
case nil
α : Type u_1
xs ys : List α
⊢ [].sym2 ~ [].sym2

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
xs ys : List α
x : α
l₁✝ l₂✝ : List α
h : l₁✝ ~ l₂✝
ih : l₁✝.sym2 ~ l₂✝.sym2
⊢ (x :: l₁✝).sym2 ~ (x :: l₂✝).sym2

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

Result:
case cons
α : Type u_1
xs ys : List α
x : α
l₁✝ l₂✝ : List α
h : l₁✝ ~ l₂✝
ih : l₁✝.sym2 ~ l₂✝.sym2
⊢ List.map (fun y => s(x, y)) l₁✝ ++ l₁✝.sym2 ~ List.map (fun y => s(x, y)) l₂✝ ++ l₂✝.sym2

Proof state:
case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ s(y, y) :: s(x, y) :: (List.map (fun y_1 => s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y => s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: s(x, y) :: (List.map (fun y => s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 => s(y, y_1)) xs ++ xs.sym2))

Tactic:
refine Perm.trans (Perm.swap ..) (Perm.trans (Perm.cons _ ?_) (Perm.swap ..))

Result:
case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ s(y, y) :: (List.map (fun y_1 => s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y => s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: (List.map (fun y => s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 => s(y, y_1)) xs ++ xs.sym2))

Proof state:
case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ {s(y, y)} + (↑(List.map (fun y_1 => s(y, y_1)) xs) + ({s(x, x)} + (↑(List.map (fun y => s(x, y)) xs) + ↑xs.sym2))) =
    {s(x, x)} + (↑(List.map (fun y => s(x, y)) xs) + ({s(y, y)} + (↑(List.map (fun y_1 => s(y, y_1)) xs) + ↑xs.sym2)))

Tactic:
simp only [add_assoc, add_left_comm]

Result:
no goals

Proof state:
case cons
α : Type u_1
xs ys : List α
x : α
l₁✝ l₂✝ : List α
h : l₁✝ ~ l₂✝
ih : l₁✝.sym2 ~ l₂✝.sym2
⊢ List.map (fun y => s(x, y)) l₁✝ ++ l₁✝.sym2 ~ List.map (fun y => s(x, y)) l₂✝ ++ l₂✝.sym2

Tactic:
exact (h.map _).append ih

Result:
no goals

Proof state:
case trans
α : Type u_1
xs ys l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih1 : l₁✝.sym2 ~ l₂✝.sym2
ih2 : l₂✝.sym2 ~ l₃✝.sym2
⊢ l₁✝.sym2 ~ l₃✝.sym2

Tactic:
exact ih1.trans ih2

Result:
no goals

Proof state:
case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ s(y, y) :: (List.map (fun y_1 => s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y => s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: (List.map (fun y => s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 => s(y, y_1)) xs ++ xs.sym2))

Tactic:
simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe,
  ← Multiset.coe_add, ← Multiset.singleton_add]

Result:
case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ {s(y, y)} + (↑(List.map (fun y_1 => s(y, y_1)) xs) + ({s(x, x)} + (↑(List.map (fun y => s(x, y)) xs) + ↑xs.sym2))) =
    {s(x, x)} + (↑(List.map (fun y => s(x, y)) xs) + ({s(y, y)} + (↑(List.map (fun y_1 => s(y, y_1)) xs) + ↑xs.sym2)))

Proof state:
case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ (y :: x :: xs).sym2 ~ (x :: y :: xs).sym2

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

Result:
case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ s(y, y) :: s(y, x) :: (List.map (fun y_1 => s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y => s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: s(x, y) :: (List.map (fun y => s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 => s(y, y_1)) xs ++ xs.sym2))